Theorem uneq12d 4118

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903

This theorem is referenced by:  symdifeq1  4204  csbun  4390  csbprg  4663  disjpr2  4667  diftpsn3  4755  iunxprg  5048  relresdm1  5988  rnpropg  6176  suceqd  6380  fntpg  6548  foun  6788  f1oprswap  6815  fnimapr  6913  fnimatpd  6914  xpprsng  7081  residpr  7084  fvsnun2  7125  fsnunfv  7129  fsnunres  7130  f1ounsn  7214  f1ofvswap  7248  xpord2pred  8083  xpord3pred  8090  frrlem12  8235  oarec  8485  ereq1  8637  mapunen  9068  cnfcomlem  9598  trcl  9627  djueq12  9806  r0weon  9912  infxpen  9914  cfsmolem  10170  cfsmo  10171  axdc3lem4  10353  ttukeylem3  10411  ttukey2g  10416  alephadd  10477  fpwwe2lem12  10542  wunex2  10638  wuncval2  10647  inar1  10675  prunioo  13385  fztp  13484  fzsuc2  13486  fseq1p1m1  13502  s3tpop  14820  s4dom  14830  s2rn  14874  s3rn  14875  s7rn  14876  trclun  14925  relexp0g  14933  relexpsucnnr  14936  dfrtrcl2  14973  setsvalg  17081  setsdm  17085  setsfun0  17087  setsid  17122  prdsval  17363  imasval  17419  mreexd  17552  mreexexlemd  17554  estrreslem2  18048  ipoval  18440  istsr  18493  mndpsuppss  18677  gsumzaddlem  19837  pwssplit1  20997  psrval  21856  psdmullem  22083  ordtval  23107  ordtcnv  23119  paste  23212  connsuba  23338  ptval2  23519  dfac14  23536  xkoptsub  23572  ptuncnv  23725  ptunhmeo  23726  xpstopnlem1  23727  alexsubALTlem3  23967  ustuqtop1  24159  rrxmvallem  25334  ovolioo  25499  uniiccdif  25509  itgsplitioo  25769  limcfval  25803  lhop2  25950  lgsquadlem2  27322  nodenselem5  27630  nosupbnd2lem1  27657  nosupbnd2  27658  noinfbnd2lem1  27672  noinfbnd2  27673  noetainflem2  27680  madeoldsuc  27833  lrold  27845  lrrecval  27885  addsval  27908  addsrid  27910  addscom  27912  addsproplem1  27915  addsprop  27922  addsass  27951  mulsval  28051  mulsrid  28055  mulsproplemcbv  28057  mulsproplem1  28058  mulsprop  28072  mulscom  28081  addsdi  28097  mulsass  28108  mulsunif2lem  28111  precsexlemcbv  28147  precsexlem3  28150  n0scut  28265  halfcut  28381  pw2cut2  28385  readdscl  28404  remulscl  28407  axlowdimlem13  28936  axlowdimlem15  28938  axlowdim  28943  eengv  28961  vtxdun  29464  trlsegvdeg  30211  numclwwlk3lem2lem  30367  ex-res  30425  imadifxp  32585  suppun2  32671  cnvprop  32683  mptprop  32685  coprprop  32686  fmptunsnop  32687  padct  32707  resf1o  32719  symgcom  33061  tocycfv  33087  tocycf  33095  tocyc01  33096  cycpm2tr  33097  cycpmco2f1  33102  cycpmco2rn  33103  cycpmconjv  33120  cycpmconjslem2  33133  elrgspnlem4  33221  rlocval  33235  idlsrgval  33477  rprmval  33490  extvfvcl  33589  zarclsun  33906  ordtprsval  33954  ordtprsuni  33955  ordtcnvNEW  33956  unelcarsg  34348  carsgclctunlem1  34353  eulerpartlemt  34407  sseqval  34424  probun  34455  bnj1373  35065  bnj1489  35091  cvmliftlem10  35361  satfvsuc  35428  satfdm  35436  satf0suc  35443  sat1el2xp  35446  fmlasuc0  35451  satffunlem1lem1  35469  satffunlem2lem1  35471  mrexval  35568  mrsubffval  35574  msrval  35605  mthmpps  35649  lineunray  36214  rdgssun  37445  exrecfnlem  37446  finixpnum  37668  ptrest  37682  poimirlem1  37684  poimirlem2  37685  poimirlem3  37686  poimirlem4  37687  poimirlem5  37688  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem9  37692  poimirlem10  37693  poimirlem11  37694  poimirlem12  37695  poimirlem15  37698  poimirlem16  37699  poimirlem17  37700  poimirlem18  37701  poimirlem19  37702  poimirlem20  37703  poimirlem21  37704  poimirlem22  37705  poimirlem23  37706  poimirlem24  37707  poimirlem26  37709  poimirlem27  37710  poimirlem28  37711  poimirlem32  37715  mblfinlem2  37721  itg2addnclem2  37735  ecun  38440  ecuncnvepres  38442  ldualset  39247  paddval  39920  paddcom  39935  dvafset  41126  dvaset  41127  dvhfset  41202  dvhset  41203  hdmapfval  41949  hlhilset  42056  dvun  42480  fsuppssindlem2  42713  istopclsd  42820  fzsplit1nn0  42874  diophrw  42879  eldioph2lem1  42880  eldioph2lem2  42881  diophin  42892  diophren  42933  pwssplit4  43209  mendval  43299  iocunico  43331  tfsconcatun  43457  tfsconcat0i  43465  onsucunitp  43493  oaun3  43502  rclexi  43735  rtrclex  43737  rtrclexi  43741  cnvrcl0  43745  dfrtrcl5  43749  dfrcl2  43794  dfrcl3  43795  iunrelexp0  43822  trclfvdecomr  43848  dfrtrcl4  43858  frege131d  43884  clsk3nimkb  44160  clsk1indlem3  44163  clsk1independent  44166  ntrclskb  44189  ntrclsk3  44190  ntrclsk13  44191  permaxinf2lem  45132  dvmptfprodlem  46069  caratheodorylem1  46651  ovnsubadd2lem  46770  ovolval4lem1  46774  fzopredsuc  47450  clnbgrval  47949  cycl3grtri  48074  aacllem  49929