What is the quantified definition for proper subset

We're thinking its:

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

is this OK?

Thanks,

z.

-
Yes, that works. –  Brian M. Scott Jul 4 '12 at 17:19

As Brian says: Yes, that works. ${}{}{}{}{}{}{}{}{}{}{}{}{}{}$

-
Great! I was wondering, why did you include dollar{}{}{}{}{}{}dollar in your answer? –  Ziggy Jul 4 '12 at 17:37
An answer has to contain some minimum number of characters before the system will accept it. Since my first attempt to submit it had too few characters, I added some do-nothing TeX code to mollify the server. –  Henning Makholm Jul 4 '12 at 17:44
You could use the axiom of extensionality to make a simpler definition: $$A\subsetneq B =_\mathrm{def} (\forall x\in A. x\in B)\land \lnot(A=B).$$