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) (Proof shortened by BJ, 23-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		nsb	|- ( A. y -. F. -> -. [ x / y ] F. )
2		fal	|- -. F.
3	1 2	mpg	|- -. [ x / y ] F.
4		dfnul4	|- (/) = { y | F. }
5	4	eleq2i	|- ( x e. (/) <-> x e. { y | F. } )
6		df-clab	|- ( x e. { y | F. } <-> [ x / y ] F. )
7	5 6	bitri	|- ( x e. (/) <-> [ x / y ] F. )
8	3 7	mtbir	|- -. x e. (/)
9	8	intnan	|- -. ( x = A /\ x e. (/) )
10	9	nex	|- -. E. x ( x = A /\ x e. (/) )
11		dfclel	|- ( A e. (/) <-> E. x ( x = A /\ x e. (/) ) )
12	10 11	mtbir	|- -. A e. (/)