Theorem 0un

Description: The union of the empty set with a class is itself. Commuted form of un0 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	0un	$$⊢\varnothing \cup A=A$$

Proof

Step	Hyp	Ref	Expression
1		uncom	$$⊢\varnothing \cup A=A\cup \varnothing$$
2		un0	$$⊢A\cup \varnothing =A$$
3	1 2	eqtri	$$⊢\varnothing \cup A=A$$