Theorem uneq12d 4144

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931

This theorem is referenced by:  symdifeq1  4230  csbun  4416  csbprg  4685  disjpr2  4689  diftpsn3  4778  iunxprg  5072  relresdm1  6020  rnpropg  6211  suceq  6419  fntpg  6596  foun  6836  f1oprswap  6862  fnimapr  6962  fnimatpd  6963  xpprsng  7130  residpr  7133  fvsnun2  7175  fsnunfv  7179  fsnunres  7180  f1ounsn  7265  f1ofvswap  7299  xpord2pred  8144  xpord3pred  8151  frrlem12  8296  oarec  8574  ereq1  8726  mapunen  9160  cnfcomlem  9713  trcl  9742  djueq12  9918  r0weon  10026  infxpen  10028  cfsmolem  10284  cfsmo  10285  axdc3lem4  10467  ttukeylem3  10525  ttukey2g  10530  alephadd  10591  fpwwe2lem12  10656  wunex2  10752  wuncval2  10761  inar1  10789  prunioo  13498  fztp  13597  fzsuc2  13599  fseq1p1m1  13615  s3tpop  14928  s4dom  14938  s2rn  14982  s3rn  14983  s7rn  14984  trclun  15033  relexp0g  15041  relexpsucnnr  15044  dfrtrcl2  15081  setsvalg  17185  setsdm  17189  setsfun0  17191  setsid  17226  prdsval  17469  imasval  17525  mreexd  17654  mreexexlemd  17656  estrreslem2  18150  ipoval  18540  istsr  18593  mndpsuppss  18743  gsumzaddlem  19902  pwssplit1  21017  psrval  21875  psdmullem  22103  ordtval  23127  ordtcnv  23139  paste  23232  connsuba  23358  ptval2  23539  dfac14  23556  xkoptsub  23592  ptuncnv  23745  ptunhmeo  23746  xpstopnlem1  23747  alexsubALTlem3  23987  ustuqtop1  24180  rrxmvallem  25356  ovolioo  25521  uniiccdif  25531  itgsplitioo  25791  limcfval  25825  lhop2  25972  lgsquadlem2  27344  nodenselem5  27652  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd2lem1  27694  noinfbnd2  27695  noetainflem2  27702  madeoldsuc  27848  lrold  27860  lrrecval  27898  addsval  27921  addsrid  27923  addscom  27925  addsproplem1  27928  addsprop  27935  addsass  27964  mulsval  28064  mulsrid  28068  mulsproplemcbv  28070  mulsproplem1  28071  mulsprop  28085  mulscom  28094  addsdi  28110  mulsass  28121  mulsunif2lem  28124  precsexlemcbv  28160  precsexlem3  28163  n0scut  28278  halfcut  28385  readdscl  28402  remulscl  28405  axlowdimlem13  28933  axlowdimlem15  28935  axlowdim  28940  eengv  28958  vtxdun  29461  trlsegvdeg  30208  numclwwlk3lem2lem  30364  ex-res  30422  imadifxp  32582  suppun2  32661  cnvprop  32673  mptprop  32675  coprprop  32676  fmptunsnop  32677  padct  32697  resf1o  32707  symgcom  33094  tocycfv  33120  tocycf  33128  tocyc01  33129  cycpm2tr  33130  cycpmco2f1  33135  cycpmco2rn  33136  cycpmconjv  33153  cycpmconjslem2  33166  elrgspnlem4  33240  rlocval  33254  idlsrgval  33518  rprmval  33531  zarclsun  33901  ordtprsval  33949  ordtprsuni  33950  ordtcnvNEW  33951  unelcarsg  34344  carsgclctunlem1  34349  eulerpartlemt  34403  sseqval  34420  probun  34451  bnj1373  35061  bnj1489  35087  cvmliftlem10  35316  satfvsuc  35383  satfdm  35391  satf0suc  35398  sat1el2xp  35401  fmlasuc0  35406  satffunlem1lem1  35424  satffunlem2lem1  35426  mrexval  35523  mrsubffval  35529  msrval  35560  mthmpps  35604  lineunray  36165  rdgssun  37396  exrecfnlem  37397  finixpnum  37629  ptrest  37643  poimirlem1  37645  poimirlem2  37646  poimirlem3  37647  poimirlem4  37648  poimirlem5  37649  poimirlem6  37650  poimirlem7  37651  poimirlem8  37652  poimirlem9  37653  poimirlem10  37654  poimirlem11  37655  poimirlem12  37656  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem18  37662  poimirlem19  37663  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem23  37667  poimirlem24  37668  poimirlem26  37670  poimirlem27  37671  poimirlem28  37672  poimirlem32  37676  mblfinlem2  37682  itg2addnclem2  37696  ldualset  39143  paddval  39817  paddcom  39832  dvafset  41023  dvaset  41024  dvhfset  41099  dvhset  41100  hdmapfval  41846  hlhilset  41953  metakunt17  42234  metakunt20  42237  metakunt21  42238  metakunt22  42239  metakunt24  42241  dvun  42402  fsuppssindlem2  42615  istopclsd  42723  fzsplit1nn0  42777  diophrw  42782  eldioph2lem1  42783  eldioph2lem2  42784  diophin  42795  diophren  42836  pwssplit4  43113  mendval  43203  iocunico  43235  tfsconcatun  43361  tfsconcat0i  43369  onsucunitp  43397  oaun3  43406  rclexi  43639  rtrclex  43641  rtrclexi  43645  cnvrcl0  43649  dfrtrcl5  43653  dfrcl2  43698  dfrcl3  43699  iunrelexp0  43726  trclfvdecomr  43752  dfrtrcl4  43762  frege131d  43788  clsk3nimkb  44064  clsk1indlem3  44067  clsk1independent  44070  ntrclskb  44093  ntrclsk3  44094  ntrclsk13  44095  permaxinf2lem  45037  dvmptfprodlem  45973  caratheodorylem1  46555  ovnsubadd2lem  46674  ovolval4lem1  46678  fzopredsuc  47352  clnbgrval  47836  cycl3grtri  47959  aacllem  49665