Theorem uneq12d 3645

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 3639	. 2 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4	1, 2, 3	syl2anc 659	1 |- ( ph -> ( A u. C ) = ( B u. D ) )

Syntax hints:   -> wi 4   = wceq 1398   u. cun 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466

This theorem is referenced by:  symdifeq1  3717  csbun  3848  csbprg  4075  disjpr2  4078  diftpsn3  4154  suceq  4932  rnpropg  5471  fntpg  5625  foun  5816  f1oprswap  5837  fnimapr  5912  residpr  6051  fsnunfv  6087  fsnunres  6088  oarec  7203  ereq1  7310  mapunen  7679  cnfcomlem  8134  cnfcomlemOLD  8142  trcl  8150  r0weon  8381  infxpen  8383  cfsmolem  8641  cfsmo  8642  axdc3lem4  8824  ttukeylem3  8882  ttukey2g  8887  alephadd  8943  fpwwe2lem13  9009  wunex2  9105  wuncval2  9114  inar1  9142  prunioo  11652  fztp  11740  fzsuc2  11741  fseq1p1m1  11756  s4dom  12858  trclun  12932  relexp0g  12939  relexpsucnnr  12942  dfrtrcl2  12977  setsvalg  14740  setsid  14759  prdsval  14944  imasval  15000  mreexd  15131  mreexexlemd  15133  estrreslem2  15606  ipoval  15983  istsr  16046  gsumzaddlem  17133  pwssplit1  17900  psrval  18206  ordtval  19857  ordtcnv  19869  paste  19962  consuba  20087  ptval2  20268  dfac14  20285  xkoptsub  20321  ptuncnv  20474  ptunhmeo  20475  xpstopnlem1  20476  alexsubALTlem3  20715  ustuqtop1  20910  rrxmvallem  21997  ovolioo  22144  uniiccdif  22153  itgsplitioo  22410  limcfval  22442  lhop2  22582  lgsquadlem2  23828  axlowdimlem13  24459  axlowdimlem15  24461  axlowdim  24466  eengv  24484  constr2spthlem1  24798  constr3pthlem1  24857  constr3pthlem2  24858  vdgrun  25103  vdgrfiun  25104  ex-res  25364  imadifxp  27672  padct  27776  resf1o  27784  ordtprsval  28135  ordtprsuni  28136  ordtcnvNEW  28137  unelcarsg  28520  carsgclctunlem1  28525  eulerpartlemt  28574  sseqval  28591  probun  28622  cvmliftlem10  29003  mrexval  29125  mrsubffval  29131  msrval  29162  mthmpps  29206  lineunray  30025  finixpnum  30278  ptrest  30288  mblfinlem2  30292  itg2addnclem2  30307  istopclsd  30872  fzsplit1nn0  30926  diophrw  30931  eldioph2lem1  30932  eldioph2lem2  30933  diophin  30945  diophren  30986  pwssplit4  31274  mendval  31373  iocunico  31419  dvmptfprodlem  31980  iunxprg  32676  xpprsng  33175  mndpsuppss  33218  aacllem  33604  bnj1373  34487  bnj1489  34513  ldualset  35247  paddval  35919  paddcom  35934  dvafset  37127  dvaset  37128  dvhfset  37204  dvhset  37205  hdmapfval  37954  hlhilset  38061  dfrcl2  38193  dfrcl3  38194  dfrtrcl4  38215  iunrelexp0  38224