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.
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.
As Brian says: Yes, that works. ${}{}{}{}{}{}{}{}{}{}{}{}{}{}$
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).$
This is, of course, equivalent to yours.