Theorem uneq12d 4164

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

Hypotheses

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
uneq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
uneq12d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Proof of Theorem uneq12d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		uneq12 4158	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953

This theorem is referenced by:  symdifeq1  4244  csbun  4438  csbprg  4713  disjpr2  4717  diftpsn3  4805  iunxprg  5099  relresdm1  6033  rnpropg  6221  suceq  6430  fntpg  6608  foun  6851  f1oprswap  6877  fnimapr  6975  xpprsng  7140  residpr  7143  fvsnun2  7183  fsnunfv  7187  fsnunres  7188  f1ofvswap  7307  xpord2pred  8134  xpord3pred  8141  frrlem12  8285  oarec  8565  ereq1  8713  mapunen  9149  cnfcomlem  9697  trcl  9726  djueq12  9902  r0weon  10010  infxpen  10012  cfsmolem  10268  cfsmo  10269  axdc3lem4  10451  ttukeylem3  10509  ttukey2g  10514  alephadd  10575  fpwwe2lem12  10640  wunex2  10736  wuncval2  10745  inar1  10773  prunioo  13463  fztp  13562  fzsuc2  13564  fseq1p1m1  13580  s3tpop  14865  s4dom  14875  trclun  14966  relexp0g  14974  relexpsucnnr  14977  dfrtrcl2  15014  setsvalg  17104  setsdm  17108  setsfun0  17110  setsid  17146  prdsval  17406  imasval  17462  mreexd  17591  mreexexlemd  17593  estrreslem2  18095  ipoval  18488  istsr  18541  gsumzaddlem  19831  pwssplit1  20815  psrval  21688  ordtval  22914  ordtcnv  22926  paste  23019  connsuba  23145  ptval2  23326  dfac14  23343  xkoptsub  23379  ptuncnv  23532  ptunhmeo  23533  xpstopnlem1  23534  alexsubALTlem3  23774  ustuqtop1  23967  rrxmvallem  25153  ovolioo  25318  uniiccdif  25328  itgsplitioo  25588  limcfval  25622  lhop2  25768  lgsquadlem2  27121  nodenselem5  27428  nosupbnd2lem1  27455  nosupbnd2  27456  noinfbnd2lem1  27470  noinfbnd2  27471  noetainflem2  27478  madeoldsuc  27617  lrold  27629  lrrecval  27662  addsval  27685  addsrid  27687  addscom  27689  addsproplem1  27692  addsprop  27699  addsass  27728  mulsval  27805  mulsrid  27809  mulsproplemcbv  27811  mulsproplem1  27812  mulsprop  27826  mulscom  27835  addsdi  27850  mulsass  27861  precsexlemcbv  27892  precsexlem3  27895  n0scut  27944  axlowdimlem13  28480  axlowdimlem15  28482  axlowdim  28487  eengv  28505  vtxdun  29006  trlsegvdeg  29748  numclwwlk3lem2lem  29904  ex-res  29962  imadifxp  32100  fnimatp  32170  cnvprop  32186  mptprop  32188  coprprop  32189  padct  32212  resf1o  32223  symgcom  32515  tocycfv  32539  tocycf  32547  tocyc01  32548  cycpm2tr  32549  cycpmco2f1  32554  cycpmco2rn  32555  cycpmconjv  32572  cycpmconjslem2  32585  idlsrgval  32892  rprmval  32908  zarclsun  33149  ordtprsval  33197  ordtprsuni  33198  ordtcnvNEW  33199  unelcarsg  33610  carsgclctunlem1  33615  eulerpartlemt  33669  sseqval  33686  probun  33717  bnj1373  34340  bnj1489  34366  cvmliftlem10  34584  satfvsuc  34651  satfdm  34659  satf0suc  34666  sat1el2xp  34669  fmlasuc0  34674  satffunlem1lem1  34692  satffunlem2lem1  34694  mrexval  34791  mrsubffval  34797  msrval  34828  mthmpps  34872  lineunray  35424  rdgssun  36563  exrecfnlem  36564  finixpnum  36777  ptrest  36791  poimirlem1  36793  poimirlem2  36794  poimirlem3  36795  poimirlem4  36796  poimirlem5  36797  poimirlem6  36798  poimirlem7  36799  poimirlem8  36800  poimirlem9  36801  poimirlem10  36802  poimirlem11  36803  poimirlem12  36804  poimirlem15  36807  poimirlem16  36808  poimirlem17  36809  poimirlem18  36810  poimirlem19  36811  poimirlem20  36812  poimirlem21  36813  poimirlem22  36814  poimirlem23  36815  poimirlem24  36816  poimirlem26  36818  poimirlem27  36819  poimirlem28  36820  poimirlem32  36824  mblfinlem2  36830  itg2addnclem2  36844  ldualset  38299  paddval  38973  paddcom  38988  dvafset  40179  dvaset  40180  dvhfset  40255  dvhset  40256  hdmapfval  41002  hlhilset  41109  metakunt17  41308  metakunt20  41311  metakunt21  41312  metakunt22  41313  metakunt24  41315  fsuppssindlem2  41467  istopclsd  41741  fzsplit1nn0  41795  diophrw  41800  eldioph2lem1  41801  eldioph2lem2  41802  diophin  41813  diophren  41854  pwssplit4  42134  mendval  42228  iocunico  42263  tfsconcatun  42390  tfsconcat0i  42398  onsucunitp  42426  oaun3  42435  rclexi  42669  rtrclex  42671  rtrclexi  42675  cnvrcl0  42679  dfrtrcl5  42683  dfrcl2  42728  dfrcl3  42729  iunrelexp0  42756  trclfvdecomr  42782  dfrtrcl4  42792  frege131d  42818  clsk3nimkb  43094  clsk1indlem3  43097  clsk1independent  43100  ntrclskb  43123  ntrclsk3  43124  ntrclsk13  43125  dvmptfprodlem  44959  caratheodorylem1  45541  ovnsubadd2lem  45660  ovolval4lem1  45664  fzopredsuc  46330  mndpsuppss  47136  aacllem  47936