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 ∅ = { ∅ }