Theorem 0un

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

	Ref	Expression
Assertion	0un	⊢ ( ∅ ∪ 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( ∅ ∪ 𝐴 ) = ( 𝐴 ∪ ∅ )
2		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
3	1 2	eqtri	⊢ ( ∅ ∪ 𝐴 ) = 𝐴