Theorem suc0

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

	Ref	Expression
Assertion	suc0	$$⊢\mathrm{suc}\varnothing =\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-suc	$$⊢\mathrm{suc}\varnothing =\varnothing \cup \left\{\varnothing \right\}$$
2		uncom	$$⊢\varnothing \cup \left\{\varnothing \right\}=\left\{\varnothing \right\}\cup \varnothing$$
3		un0	$$⊢\left\{\varnothing \right\}\cup \varnothing =\left\{\varnothing \right\}$$
4	1 2 3	3eqtri	$$⊢\mathrm{suc}\varnothing =\left\{\varnothing \right\}$$