Metamath Proof Explorer

Theorem uneq12i

Description: Equality inference for the union of two classes. (Contributed by NM, 12-Aug-2004) (Proof shortened by Eric Schmidt, 26-Jan-2007)

Ref Expression
Hypotheses uneq1i.1 
|- A = B
uneq12i.2 
|- C = D
Assertion uneq12i 
|- ( A u. C ) = ( B u. D )

Proof

Step Hyp Ref Expression
1 uneq1i.1 
 |-  A = B
2 uneq12i.2 
 |-  C = D
3 uneq12 
 |-  ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4 1 2 3 mp2an 
 |-  ( A u. C ) = ( B u. D )