Theorem uneq12i 3312

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 3309	. 2 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4	1, 2, 3	mp2an 426	1 |- ( A u. C ) = ( B u. D )

Syntax hints:   = wceq 1364   u. cun 3152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158

This theorem is referenced by:  indir  3409  difundir  3413  symdif1  3425  unrab  3431  rabun2  3439  dfif6  3560  dfif3  3571  unopab  4109  xpundi  4716  xpundir  4717  xpun  4721  dmun  4870  resundi  4956  resundir  4957  cnvun  5072  rnun  5075  imaundi  5079  imaundir  5080  dmtpop  5142  coundi  5168  coundir  5169  unidmrn  5199  dfdm2  5201  mptun  5386  fpr  5741  fvsnun2  5757  sbthlemi5  7022  djuunr  7127  djuun  7128  casedm  7147  djudm  7166  djuassen  7279  fz0to3un2pr  10192  fz0to4untppr  10193  fzo0to42pr  10290  xnn0nnen  10511