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	⊢ ∃* 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥

Proof

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