Metamath Proof Explorer

Theorem unieqd

Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995)

Ref Expression
Hypothesis unieqd.1 
|- ( ph -> A = B )
Assertion unieqd 
|- ( ph -> U. A = U. B )

Proof

Step Hyp Ref Expression
1 unieqd.1 
 |-  ( ph -> A = B )
2 unieq 
 |-  ( A = B -> U. A = U. B )
3 1 2 syl 
 |-  ( ph -> U. A = U. B )