Theorem n0el

Description: Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010)

	Ref	Expression
Assertion	n0el	$$⊢\neg \varnothing \in A\leftrightarrow \forall x\in A\exists uu\in x$$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall x\in A\neg \forall u\neg u\in x\leftrightarrow \forall x\left(x\in A\to \neg \forall u\neg u\in x\right)$$
2		df-ex	$$⊢\exists uu\in x\leftrightarrow \neg \forall u\neg u\in x$$
3	2	ralbii	$$⊢\forall x\in A\exists uu\in x\leftrightarrow \forall x\in A\neg \forall u\neg u\in x$$
4		alnex	$$⊢\forall x\neg \left(x\in A\wedge \forall u\neg u\in x\right)\leftrightarrow \neg \exists x\left(x\in A\wedge \forall u\neg u\in x\right)$$
5		imnang	$$⊢\forall x\left(x\in A\to \neg \forall u\neg u\in x\right)\leftrightarrow \forall x\neg \left(x\in A\wedge \forall u\neg u\in x\right)$$
6		0el	$$⊢\varnothing \in A\leftrightarrow \exists x\in A\forall u\neg u\in x$$
7		df-rex	$$⊢\exists x\in A\forall u\neg u\in x\leftrightarrow \exists x\left(x\in A\wedge \forall u\neg u\in x\right)$$
8	6 7	bitri	$$⊢\varnothing \in A\leftrightarrow \exists x\left(x\in A\wedge \forall u\neg u\in x\right)$$
9	8	notbii	$$⊢\neg \varnothing \in A\leftrightarrow \neg \exists x\left(x\in A\wedge \forall u\neg u\in x\right)$$
10	4 5 9	3bitr4ri	$$⊢\neg \varnothing \in A\leftrightarrow \forall x\left(x\in A\to \neg \forall u\neg u\in x\right)$$
11	1 3 10	3bitr4ri	$$⊢\neg \varnothing \in A\leftrightarrow \forall x\in A\exists uu\in x$$