Metamath Proof Explorer


Theorem unieqi

Description: Inference of equality of two class unions. (Contributed by NM, 30-Aug-1993)

Ref Expression
Hypothesis unieqi.1 ⊢ A = B
Assertion unieqi ⊢ ⋃ A = ⋃ B

Proof

Step Hyp Ref Expression
1 unieqi.1 ⊢ A = B
2 unieq ⊢ A = B → ⋃ A = ⋃ B
3 1 2 ax-mp ⊢ ⋃ A = ⋃ B