Theorem uneq12d 4121

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3899

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  symdifeq1  4207  csbun  4393  csbprg  4666  disjpr2  4670  diftpsn3  4758  iunxprg  5051  relresdm1  5992  rnpropg  6180  suceqd  6384  fntpg  6552  foun  6792  f1oprswap  6819  fnimapr  6917  fnimatpd  6918  xpprsng  7085  residpr  7088  fvsnun2  7129  fsnunfv  7133  fsnunres  7134  f1ounsn  7218  f1ofvswap  7252  xpord2pred  8087  xpord3pred  8094  frrlem12  8239  oarec  8489  ereq1  8642  mapunen  9074  cnfcomlem  9608  trcl  9637  djueq12  9816  r0weon  9922  infxpen  9924  cfsmolem  10180  cfsmo  10181  axdc3lem4  10363  ttukeylem3  10421  ttukey2g  10426  alephadd  10488  fpwwe2lem12  10553  wunex2  10649  wuncval2  10658  inar1  10686  prunioo  13397  fztp  13496  fzsuc2  13498  fseq1p1m1  13514  s3tpop  14832  s4dom  14842  s2rn  14886  s3rn  14887  s7rn  14888  trclun  14937  relexp0g  14945  relexpsucnnr  14948  dfrtrcl2  14985  setsvalg  17093  setsdm  17097  setsfun0  17099  setsid  17134  prdsval  17375  imasval  17432  mreexd  17565  mreexexlemd  17567  estrreslem2  18061  ipoval  18453  istsr  18506  mndpsuppss  18690  gsumzaddlem  19850  pwssplit1  21011  psrval  21871  psdmullem  22108  ordtval  23133  ordtcnv  23145  paste  23238  connsuba  23364  ptval2  23545  dfac14  23562  xkoptsub  23598  ptuncnv  23751  ptunhmeo  23752  xpstopnlem1  23753  alexsubALTlem3  23993  ustuqtop1  24185  rrxmvallem  25360  ovolioo  25525  uniiccdif  25535  itgsplitioo  25795  limcfval  25829  lhop2  25976  lgsquadlem2  27348  nodenselem5  27656  nosupbnd2lem1  27683  nosupbnd2  27684  noinfbnd2lem1  27698  noinfbnd2  27699  noetainflem2  27706  madeoldsuc  27881  lrold  27893  lrrecval  27935  addsval  27958  addsrid  27960  addscom  27962  addsproplem1  27965  addsprop  27972  addsass  28001  mulsval  28105  mulsrid  28109  mulsproplemcbv  28111  mulsproplem1  28112  mulsprop  28126  mulscom  28135  addsdi  28151  mulsass  28162  mulsunif2lem  28165  precsexlemcbv  28202  precsexlem3  28205  n0cut  28330  halfcut  28454  pw2cut2  28458  readdscl  28495  remulscl  28498  axlowdimlem13  29027  axlowdimlem15  29029  axlowdim  29034  eengv  29052  vtxdun  29555  trlsegvdeg  30302  numclwwlk3lem2lem  30458  ex-res  30516  imadifxp  32676  fresunsn  32703  suppun2  32763  cnvprop  32775  mptprop  32777  coprprop  32778  fmptunsnop  32779  padct  32797  resf1o  32809  symgcom  33165  tocycfv  33191  tocycf  33199  tocyc01  33200  cycpm2tr  33201  cycpmco2f1  33206  cycpmco2rn  33207  cycpmconjv  33224  cycpmconjslem2  33237  elrgspnlem4  33327  rlocval  33341  idlsrgval  33584  rprmval  33597  extvfvcl  33701  zarclsun  34027  ordtprsval  34075  ordtprsuni  34076  ordtcnvNEW  34077  unelcarsg  34469  carsgclctunlem1  34474  eulerpartlemt  34528  sseqval  34545  probun  34576  bnj1373  35186  bnj1489  35212  cvmliftlem10  35488  satfvsuc  35555  satfdm  35563  satf0suc  35570  sat1el2xp  35573  fmlasuc0  35578  satffunlem1lem1  35596  satffunlem2lem1  35598  mrexval  35695  mrsubffval  35701  msrval  35732  mthmpps  35776  lineunray  36341  rdgssun  37583  exrecfnlem  37584  finixpnum  37806  ptrest  37820  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  poimirlem32  37853  mblfinlem2  37859  itg2addnclem2  37873  ecun  38578  ecuncnvepres  38580  ldualset  39385  paddval  40058  paddcom  40073  dvafset  41264  dvaset  41265  dvhfset  41340  dvhset  41341  hdmapfval  42087  hlhilset  42194  dvun  42614  fsuppssindlem2  42835  istopclsd  42942  fzsplit1nn0  42996  diophrw  43001  eldioph2lem1  43002  eldioph2lem2  43003  diophin  43014  diophren  43055  pwssplit4  43331  mendval  43421  iocunico  43453  tfsconcatun  43579  tfsconcat0i  43587  onsucunitp  43615  oaun3  43624  rclexi  43856  rtrclex  43858  rtrclexi  43862  cnvrcl0  43866  dfrtrcl5  43870  dfrcl2  43915  dfrcl3  43916  iunrelexp0  43943  trclfvdecomr  43969  dfrtrcl4  43979  frege131d  44005  clsk3nimkb  44281  clsk1indlem3  44284  clsk1independent  44287  ntrclskb  44310  ntrclsk3  44311  ntrclsk13  44312  permaxinf2lem  45253  dvmptfprodlem  46188  caratheodorylem1  46770  ovnsubadd2lem  46889  ovolval4lem1  46893  fzopredsuc  47569  clnbgrval  48068  cycl3grtri  48193  aacllem  50046