Metamath Proof Explorer

Theorem uneq1

Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion uneq1 ⊢ A = B → A ∪ C = B ∪ C

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
2 1 orbi1d ⊢ A = B → x ∈ A ∨ x ∈ C ↔ x ∈ B ∨ x ∈ C
3 elun ⊢ x ∈ A ∪ C ↔ x ∈ A ∨ x ∈ C
4 elun ⊢ x ∈ B ∪ C ↔ x ∈ B ∨ x ∈ C
5 2 3 4 3bitr4g ⊢ A = B → x ∈ A ∪ C ↔ x ∈ B ∪ C
6 5 eqrdv ⊢ A = B → A ∪ C = B ∪ C