This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. (/)