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

Metamath Proof Explorer

Theorem suc0

Description: The successor of the empty set. (Contributed by NM, 1-Feb-2005)

Ref Expression
Assertion suc0 ⊢ suc ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc ⁡ ∅ = ∅ ∪ ∅
2 uncom ⊢ ∅ ∪ ∅ = ∅ ∪ ∅
3 un0 ⊢ ∅ ∪ ∅ = ∅
4 1 2 3 3eqtri ⊢ suc ⁡ ∅ = ∅