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