Description: Equality inference for the union of two classes. (Contributed by NM, 12Aug2004) (Proof shortened by Eric Schmidt, 26Jan2007)
Ref  Expression  

Hypotheses  uneq1i.1   A = B 

uneq12i.2   C = D 

Assertion  uneq12i   ( A u. C ) = ( B u. D ) 
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 ) 