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	|- ( -. (/) e. A <-> dom ( `' _E |` A ) = A )

Proof

Step	Hyp	Ref	Expression
1		dmopab3	|- ( A. x e. A E. y y e. x <-> dom { <. x , y >. | ( x e. A /\ y e. x ) } = A )
2		n0el	|- ( -. (/) e. A <-> A. x e. A E. y y e. x )
3		cnvepres	|- ( `' _E |` A ) = { <. x , y >. | ( x e. A /\ y e. x ) }
4	3	dmeqi	|- dom ( `' _E |` A ) = dom { <. x , y >. | ( x e. A /\ y e. x ) }
5	4	eqeq1i	|- ( dom ( `' _E |` A ) = A <-> dom { <. x , y >. | ( x e. A /\ y e. x ) } = A )
6	1 2 5	3bitr4i	|- ( -. (/) e. A <-> dom ( `' _E |` A ) = A )