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 
|- U. A = U. B

Proof

Step Hyp Ref Expression
1 unieqi.1 
 |-  A = B
2 unieq 
 |-  ( A = B -> U. A = U. B )
3 1 2 ax-mp 
 |-  U. A = U. B