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 )