Theorem uneq12i 3279

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

Hypotheses

Ref	Expression
uneq1i.1	|- A = B
uneq12i.2	|- C = D

Assertion

Ref	Expression
uneq12i	|- ( A u. C ) = ( B u. D )

Proof of Theorem uneq12i

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

Syntax hints:   = wceq 1348   u. cun 3119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125

This theorem is referenced by:  indir  3376  difundir  3380  symdif1  3392  unrab  3398  rabun2  3406  dfif6  3527  dfif3  3538  unopab  4066  xpundi  4665  xpundir  4666  xpun  4670  dmun  4816  resundi  4902  resundir  4903  cnvun  5014  rnun  5017  imaundi  5021  imaundir  5022  dmtpop  5084  coundi  5110  coundir  5111  unidmrn  5141  dfdm2  5143  mptun  5327  fpr  5675  fvsnun2  5691  sbthlemi5  6934  djuunr  7039  djuun  7040  casedm  7059  djudm  7078  djuassen  7181  fz0to3un2pr  10066  fz0to4untppr  10067  fzo0to42pr  10163