Metamath Proof Explorer


Theorem unieqd

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

Ref Expression
Hypothesis unieqd.1 φA=B
Assertion unieqd φA=B

Proof

Step Hyp Ref Expression
1 unieqd.1 φA=B
2 unieq A=BA=B
3 1 2 syl φA=B