Theorem noel

Description: The empty set has no elements. Theorem 6.14 of Quine p. 44. (Contributed by NM, 21-Jun-1993) (Proof shortened by Mario Carneiro, 1-Sep-2015) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

	Ref	Expression
Assertion	noel	|- -. A e. (/)

Proof

Step	Hyp	Ref	Expression
1		pm3.24	|- -. ( y e. _V /\ -. y e. _V )
2	1	nex	|- -. E. y ( y e. _V /\ -. y e. _V )
3		df-clab	|- ( x e. { y | ( y e. _V /\ -. y e. _V ) } <-> [ x / y ] ( y e. _V /\ -. y e. _V ) )
4		spsbe	|- ( [ x / y ] ( y e. _V /\ -. y e. _V ) -> E. y ( y e. _V /\ -. y e. _V ) )
5	3 4	sylbi	|- ( x e. { y | ( y e. _V /\ -. y e. _V ) } -> E. y ( y e. _V /\ -. y e. _V ) )
6	2 5	mto	|- -. x e. { y | ( y e. _V /\ -. y e. _V ) }
7		df-nul	|- (/) = ( _V \ _V )
8		df-dif	|- ( _V \ _V ) = { y | ( y e. _V /\ -. y e. _V ) }
9	7 8	eqtri	|- (/) = { y | ( y e. _V /\ -. y e. _V ) }
10	9	eleq2i	|- ( x e. (/) <-> x e. { y | ( y e. _V /\ -. y e. _V ) } )
11	6 10	mtbir	|- -. x e. (/)
12	11	intnan	|- -. ( x = A /\ x e. (/) )
13	12	nex	|- -. E. x ( x = A /\ x e. (/) )
14		dfclel	|- ( A e. (/) <-> E. x ( x = A /\ x e. (/) ) )
15	13 14	mtbir	|- -. A e. (/)