Theorem uneq12d 4135

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 4129	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  symdifeq1  4221  csbun  4407  csbprg  4676  disjpr2  4680  diftpsn3  4769  iunxprg  5063  relresdm1  6007  rnpropg  6198  suceqd  6402  fntpg  6579  foun  6821  f1oprswap  6847  fnimapr  6947  fnimatpd  6948  xpprsng  7115  residpr  7118  fvsnun2  7160  fsnunfv  7164  fsnunres  7165  f1ounsn  7250  f1ofvswap  7284  xpord2pred  8127  xpord3pred  8134  frrlem12  8279  oarec  8529  ereq1  8681  mapunen  9116  cnfcomlem  9659  trcl  9688  djueq12  9864  r0weon  9972  infxpen  9974  cfsmolem  10230  cfsmo  10231  axdc3lem4  10413  ttukeylem3  10471  ttukey2g  10476  alephadd  10537  fpwwe2lem12  10602  wunex2  10698  wuncval2  10707  inar1  10735  prunioo  13449  fztp  13548  fzsuc2  13550  fseq1p1m1  13566  s3tpop  14882  s4dom  14892  s2rn  14936  s3rn  14937  s7rn  14938  trclun  14987  relexp0g  14995  relexpsucnnr  14998  dfrtrcl2  15035  setsvalg  17143  setsdm  17147  setsfun0  17149  setsid  17184  prdsval  17425  imasval  17481  mreexd  17610  mreexexlemd  17612  estrreslem2  18106  ipoval  18496  istsr  18549  mndpsuppss  18699  gsumzaddlem  19858  pwssplit1  20973  psrval  21831  psdmullem  22059  ordtval  23083  ordtcnv  23095  paste  23188  connsuba  23314  ptval2  23495  dfac14  23512  xkoptsub  23548  ptuncnv  23701  ptunhmeo  23702  xpstopnlem1  23703  alexsubALTlem3  23943  ustuqtop1  24136  rrxmvallem  25311  ovolioo  25476  uniiccdif  25486  itgsplitioo  25746  limcfval  25780  lhop2  25927  lgsquadlem2  27299  nodenselem5  27607  nosupbnd2lem1  27634  nosupbnd2  27635  noinfbnd2lem1  27649  noinfbnd2  27650  noetainflem2  27657  madeoldsuc  27803  lrold  27815  lrrecval  27853  addsval  27876  addsrid  27878  addscom  27880  addsproplem1  27883  addsprop  27890  addsass  27919  mulsval  28019  mulsrid  28023  mulsproplemcbv  28025  mulsproplem1  28026  mulsprop  28040  mulscom  28049  addsdi  28065  mulsass  28076  mulsunif2lem  28079  precsexlemcbv  28115  precsexlem3  28118  n0scut  28233  halfcut  28340  readdscl  28357  remulscl  28360  axlowdimlem13  28888  axlowdimlem15  28890  axlowdim  28895  eengv  28913  vtxdun  29416  trlsegvdeg  30163  numclwwlk3lem2lem  30319  ex-res  30377  imadifxp  32537  suppun2  32614  cnvprop  32626  mptprop  32628  coprprop  32629  fmptunsnop  32630  padct  32650  resf1o  32660  symgcom  33047  tocycfv  33073  tocycf  33081  tocyc01  33082  cycpm2tr  33083  cycpmco2f1  33088  cycpmco2rn  33089  cycpmconjv  33106  cycpmconjslem2  33119  elrgspnlem4  33203  rlocval  33217  idlsrgval  33481  rprmval  33494  zarclsun  33867  ordtprsval  33915  ordtprsuni  33916  ordtcnvNEW  33917  unelcarsg  34310  carsgclctunlem1  34315  eulerpartlemt  34369  sseqval  34386  probun  34417  bnj1373  35027  bnj1489  35053  cvmliftlem10  35288  satfvsuc  35355  satfdm  35363  satf0suc  35370  sat1el2xp  35373  fmlasuc0  35378  satffunlem1lem1  35396  satffunlem2lem1  35398  mrexval  35495  mrsubffval  35501  msrval  35532  mthmpps  35576  lineunray  36142  rdgssun  37373  exrecfnlem  37374  finixpnum  37606  ptrest  37620  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem32  37653  mblfinlem2  37659  itg2addnclem2  37673  ldualset  39125  paddval  39799  paddcom  39814  dvafset  41005  dvaset  41006  dvhfset  41081  dvhset  41082  hdmapfval  41828  hlhilset  41935  dvun  42354  fsuppssindlem2  42587  istopclsd  42695  fzsplit1nn0  42749  diophrw  42754  eldioph2lem1  42755  eldioph2lem2  42756  diophin  42767  diophren  42808  pwssplit4  43085  mendval  43175  iocunico  43207  tfsconcatun  43333  tfsconcat0i  43341  onsucunitp  43369  oaun3  43378  rclexi  43611  rtrclex  43613  rtrclexi  43617  cnvrcl0  43621  dfrtrcl5  43625  dfrcl2  43670  dfrcl3  43671  iunrelexp0  43698  trclfvdecomr  43724  dfrtrcl4  43734  frege131d  43760  clsk3nimkb  44036  clsk1indlem3  44039  clsk1independent  44042  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  permaxinf2lem  45009  dvmptfprodlem  45949  caratheodorylem1  46531  ovnsubadd2lem  46650  ovolval4lem1  46654  fzopredsuc  47328  clnbgrval  47827  cycl3grtri  47950  aacllem  49794