Quantified definition for "not a proper subset"

Question

The quantified definition for a proper subset can be found here.

$A \subset B \leftrightarrow \forall x [x \in A \rightarrow x \in B] \land \exists x [x \notin A \land x \in B]$

I want to determine $A \not \subset B$ (A not proper subset B). Can I simply negate $A \subset B$ for $A \not \subset B$? $$\neg \Big(\forall x [x \in A \rightarrow x \in B] \land \exists x [x \notin A \land x \in B]\Big) \\ \leftrightarrow \neg \Big(\forall x [\neg (x \in A) \vee x \in B] \land \exists x [x \notin A \land x \in B]\Big) \\ \leftrightarrow \exists x [x \in A \wedge x \notin B] \vee \forall x [x \in A \vee x \notin B]$$ The part before the first $\vee$ looks correct, but I'm not so sure for the second part: $... \vee \forall x [x \in A \vee x \notin B]$

Answer 1

Yes, that's the correct negation, though you can take one more step and express the last universal as a quantified implication .

$$\begin{array}{rcl} &&\neg \Big(\big(\forall x~[x \in A \to x \in B]\big) ~\land~ \big(\exists x~[x \notin A \land x \in B]\big)\Big) \\ &\iff& \big(\exists x~[x \in A \wedge x \notin B]\big)~\vee~\big(\forall x~[x \in A \vee x \notin B]\big)\\&\iff&\big(\exists x~[x \in A \wedge x \notin B]\big)~\vee~\big(\forall x~[x\in B\to x \in A]\big)\end{array}$$

Which looks similar to the original, except that it is a disjunction.

$A$ is not a subset of $B$ iif there is an element in $A$ that is not in $B$, or every element in $B$ is in $A$.   That effectively says: "There are bits of $A$ outside $B$ or they are actually the same set".

$$\begin{array}{rcl} \neg(A\subset B) &\iff&\neg(A\subseteq B~\wedge~B\nsubseteq A ) \\ A\not\subset B&\iff& A\nsubseteq B~\vee~B\subseteq A\end{array}$$

Answer 2

The second quantifier is needed to handle cases where $A=B$ (i.e. the equivalence case that distinguishes $\subset$ from $\subseteq$). It is easy to check that in this case, the first quantifier is false but the second one is true.