Theorem uneq12d 3530

Description: Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
uneq1d.1	|- ( ph -> A = B )
uneq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
uneq12d	|- ( ph -> ( A u. C ) = ( B u. D ) )

Proof of Theorem uneq12d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 |- ( ph -> A = B )
2		uneq12d.2	. 2 |- ( ph -> C = D )
3		uneq12 3524	. 2 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( A u. C ) = ( B u. D ) )

Syntax hints:   -> wi 4   = wceq 1369   u. cun 3345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2993  df-un 3352

This theorem is referenced by:  csbun  3728  csbungOLD  3729  disjpr2  3957  diftpsn3  4031  suceq  4803  rnpropg  5338  fntpg  5492  foun  5678  f1oprswap  5699  fnimapr  5774  residpr  5905  fsnunfv  5937  fsnunres  5938  oarec  7020  ereq1  7127  mapunen  7499  cnfcomlem  7951  cnfcomlemOLD  7959  trcl  7967  r0weon  8198  infxpen  8200  cfsmolem  8458  cfsmo  8459  axdc3lem4  8641  ttukeylem3  8699  ttukey2g  8704  alephadd  8760  fpwwe2lem13  8828  wunex2  8924  wuncval2  8933  inar1  8961  prunioo  11433  fztp  11531  fzsuc2  11533  fseq1p1m1  11553  s4dom  12548  setsvalg  14216  setsid  14234  prdsval  14412  imasval  14468  mreexd  14599  mreexexlemd  14601  ipoval  15343  istsr  15406  gsumzaddlem  16427  pwssplit1  17159  psrval  17448  ordtval  18812  ordtcnv  18824  paste  18917  consuba  19043  ptval2  19193  dfac14  19210  xkoptsub  19246  ptuncnv  19399  ptunhmeo  19400  xpstopnlem1  19401  alexsubALTlem3  19640  ustuqtop1  19835  rrxmvallem  20922  ovolioo  21068  uniiccdif  21077  itgsplitioo  21334  limcfval  21366  lhop2  21506  lgsquadlem2  22713  axlowdimlem13  23219  axlowdimlem15  23221  axlowdim  23226  eengv  23244  constr2spthlem1  23512  constr3pthlem1  23560  constr3pthlem2  23561  vdgrun  23590  vdgrfiun  23591  ex-res  23667  imadifxp  25958  resf1o  26049  ordtprsval  26367  ordtprsuni  26368  ordtcnvNEW  26369  eulerpartlemt  26773  sseqval  26790  probun  26821  cvmliftlem10  27202  dfrtrcl2  27369  symdifeq1  27870  lineunray  28197  finixpnum  28437  ptrest  28448  mblfinlem2  28452  itg2addnclem2  28467  istopclsd  29059  fzsplit1nn0  29115  diophrw  29120  eldioph2lem1  29121  eldioph2lem2  29122  diophin  29134  diophren  29175  pwssplit4  29465  mendval  29563  iocunico  29609  csbprg  30140  iunxprg  30157  xpprsng  30742  mndpsuppss  30807  bnj1373  32044  bnj1489  32070  ldualset  32793  paddval  33465  paddcom  33480  dvafset  34671  dvaset  34672  dvhfset  34748  dvhset  34749  hdmapfval  35498  hlhilset  35605