Theorem n0el2

Description: Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 31-Jan-2018)

	Ref	Expression
Assertion	n0el2	$$⊢\neg \varnothing \in A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		dmopab3	$$⊢\forall x\in A\exists yy\in x\leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}=A$$
2		n0el	$$⊢\neg \varnothing \in A\leftrightarrow \forall x\in A\exists yy\in x$$
3		cnvepres	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$
4	3	dmeqi	$$⊢\mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}$$
5	4	eqeq1i	$$⊢\mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A\leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge y\in x\right)\right\}=A$$
6	1 2 5	3bitr4i	$$⊢\neg \varnothing \in A\leftrightarrow \mathrm{dom}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)=A$$