Theorem n0elim

Description: Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024)

	Ref	Expression
Assertion	n0elim	|- ( -. (/) 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 )