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

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 ⊢ ∃* x ∀ y ¬ y ∈ x

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x ⊥
2 1 axextmo ⊢ ∃* x ∀ y y ∈ x ↔ ⊥
3 nbfal ⊢ ¬ y ∈ x ↔ y ∈ x ↔ ⊥
4 3 albii ⊢ ∀ y ¬ y ∈ x ↔ ∀ y y ∈ x ↔ ⊥
5 4 mobii ⊢ ∃* x ∀ y ¬ y ∈ x ↔ ∃* x ∀ y y ∈ x ↔ ⊥
6 2 5 mpbir ⊢ ∃* x ∀ y ¬ y ∈ x