Theorem n0el3

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

	Ref	Expression
Assertion	n0el3	|- ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		n0el2	|- ( -. (/) e. A <-> dom ( `' _E |` A ) = A )
2	1	biimpi	|- ( -. (/) e. A -> dom ( `' _E |` A ) = A )
3	2	qseq1d	|- ( -. (/) e. A -> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = ( A /. ( `' _E |` A ) ) )
4		qsresid	|- ( A /. ( `' _E |` A ) ) = ( A /. `' _E )
5		qsid	|- ( A /. `' _E ) = A
6	4 5	eqtri	|- ( A /. ( `' _E |` A ) ) = A
7	3 6	eqtrdi	|- ( -. (/) e. A -> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A )
8		n0eldmqseq	|- ( ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A -> -. (/) e. A )
9	7 8	impbii	|- ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A )