Metamath Proof Explorer


Theorem nulmo

Description: There exists at most one empty set. With either axnul or axnulALT or ax-nul , this proves that there exists a unique empty set. In practice, once the language of classes is available, we use the stronger characterization among classes eq0 . (Contributed by NM, 22-Dec-2007) Use the at-most-one quantifier. (Revised by BJ, 17-Sep-2022) (Proof shortened by Wolf Lammen, 26-Apr-2023)

Ref Expression
Assertion nulmo
|- E* x A. y -. y e. x

Proof

Step Hyp Ref Expression
1 nfv
 |-  F/ x F.
2 1 axextmo
 |-  E* x A. y ( y e. x <-> F. )
3 nbfal
 |-  ( -. y e. x <-> ( y e. x <-> F. ) )
4 3 albii
 |-  ( A. y -. y e. x <-> A. y ( y e. x <-> F. ) )
5 4 mobii
 |-  ( E* x A. y -. y e. x <-> E* x A. y ( y e. x <-> F. ) )
6 2 5 mpbir
 |-  E* x A. y -. y e. x