Metamath Proof Explorer

Theorem un0

Description: The union of a class with the empty set is itself. Theorem 24 of Suppes p. 27. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion un0 ( 𝐴 ∪ ∅ ) = 𝐴

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ 𝑥 ∈ ∅
2 1 biorfri ⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅ ) )
3 2 bicomi ⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅ ) ↔ 𝑥 ∈ 𝐴 )
4 3 uneqri ⊢ ( 𝐴 ∪ ∅ ) = 𝐴