Theorem 0el

Description: Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004)

	Ref	Expression
Assertion	0el	$$⊢\varnothing \in A\leftrightarrow \exists x\in A\forall y\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		risset	$$⊢\varnothing \in A\leftrightarrow \exists x\in Ax=\varnothing$$
2		eq0	$$⊢x=\varnothing \leftrightarrow \forall y\neg y\in x$$
3	2	rexbii	$$⊢\exists x\in Ax=\varnothing \leftrightarrow \exists x\in A\forall y\neg y\in x$$
4	1 3	bitri	$$⊢\varnothing \in A\leftrightarrow \exists x\in A\forall y\neg y\in x$$