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

Metamath Proof Explorer

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 ⊢ ∅ ∪ A = A

Proof

Step Hyp Ref Expression
1 uncom ⊢ ∅ ∪ A = A ∪ ∅
2 un0 ⊢ A ∪ ∅ = A
3 1 2 eqtri ⊢ ∅ ∪ A = A