Theorem uneq12d 4110

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  symdifeq1  4196  csbun  4382  csbprg  4654  disjpr2  4658  diftpsn3  4746  iunxprg  5039  relresdm1  5990  rnpropg  6178  suceqd  6382  fntpg  6550  foun  6790  f1oprswap  6817  fnimapr  6915  fnimatpd  6916  xpprsng  7085  residpr  7088  fvsnun2  7129  fsnunfv  7133  fsnunres  7134  f1ounsn  7218  f1ofvswap  7252  xpord2pred  8086  xpord3pred  8093  frrlem12  8238  oarec  8488  ereq1  8642  mapunen  9075  cnfcomlem  9609  trcl  9638  djueq12  9817  r0weon  9923  infxpen  9925  cfsmolem  10181  cfsmo  10182  axdc3lem4  10364  ttukeylem3  10422  ttukey2g  10427  alephadd  10489  fpwwe2lem12  10554  wunex2  10650  wuncval2  10659  inar1  10687  prunioo  13423  fztp  13523  fzsuc2  13525  fseq1p1m1  13541  s3tpop  14860  s4dom  14870  s2rn  14914  s3rn  14915  s7rn  14916  trclun  14965  relexp0g  14973  relexpsucnnr  14976  dfrtrcl2  15013  setsvalg  17125  setsdm  17129  setsfun0  17131  setsid  17166  prdsval  17407  imasval  17464  mreexd  17597  mreexexlemd  17599  estrreslem2  18093  ipoval  18485  istsr  18538  mndpsuppss  18722  gsumzaddlem  19885  pwssplit1  21044  psrval  21903  psdmullem  22140  ordtval  23163  ordtcnv  23175  paste  23268  connsuba  23394  ptval2  23575  dfac14  23592  xkoptsub  23628  ptuncnv  23781  ptunhmeo  23782  xpstopnlem1  23783  alexsubALTlem3  24023  ustuqtop1  24215  rrxmvallem  25380  ovolioo  25544  uniiccdif  25554  itgsplitioo  25814  limcfval  25848  lhop2  25992  lgsquadlem2  27363  nodenselem5  27671  nosupbnd2lem1  27698  nosupbnd2  27699  noinfbnd2lem1  27713  noinfbnd2  27714  noetainflem2  27721  madeoldsuc  27896  lrold  27908  lrrecval  27950  addsval  27973  addsrid  27975  addscom  27977  addsproplem1  27980  addsprop  27987  addsass  28016  mulsval  28120  mulsrid  28124  mulsproplemcbv  28126  mulsproplem1  28127  mulsprop  28141  mulscom  28150  addsdi  28166  mulsass  28177  mulsunif2lem  28180  precsexlemcbv  28217  precsexlem3  28220  n0cut  28345  halfcut  28469  pw2cut2  28473  readdscl  28510  remulscl  28513  axlowdimlem13  29042  axlowdimlem15  29044  axlowdim  29049  eengv  29067  vtxdun  29570  trlsegvdeg  30317  numclwwlk3lem2lem  30473  ex-res  30531  imadifxp  32691  fresunsn  32718  suppun2  32777  cnvprop  32789  mptprop  32791  coprprop  32792  fmptunsnop  32793  padct  32811  resf1o  32823  symgcom  33164  tocycfv  33190  tocycf  33198  tocyc01  33199  cycpm2tr  33200  cycpmco2f1  33205  cycpmco2rn  33206  cycpmconjv  33223  cycpmconjslem2  33236  elrgspnlem4  33326  rlocval  33340  idlsrgval  33583  rprmval  33596  extvfvcl  33700  zarclsun  34035  ordtprsval  34083  ordtprsuni  34084  ordtcnvNEW  34085  unelcarsg  34477  carsgclctunlem1  34482  eulerpartlemt  34536  sseqval  34553  probun  34584  bnj1373  35193  bnj1489  35219  cvmliftlem10  35497  satfvsuc  35564  satfdm  35572  satf0suc  35579  sat1el2xp  35582  fmlasuc0  35587  satffunlem1lem1  35605  satffunlem2lem1  35607  mrexval  35704  mrsubffval  35710  msrval  35741  mthmpps  35785  lineunray  36350  rdgssun  37705  exrecfnlem  37706  finixpnum  37937  ptrest  37951  poimirlem1  37953  poimirlem2  37954  poimirlem3  37955  poimirlem4  37956  poimirlem5  37957  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem9  37961  poimirlem10  37962  poimirlem11  37963  poimirlem12  37964  poimirlem15  37967  poimirlem16  37968  poimirlem17  37969  poimirlem18  37970  poimirlem19  37971  poimirlem20  37972  poimirlem21  37973  poimirlem22  37974  poimirlem23  37975  poimirlem24  37976  poimirlem26  37978  poimirlem27  37979  poimirlem28  37980  poimirlem32  37984  mblfinlem2  37990  itg2addnclem2  38004  ecun  38725  ecuncnvepres  38727  ldualset  39582  paddval  40255  paddcom  40270  dvafset  41461  dvaset  41462  dvhfset  41537  dvhset  41538  hdmapfval  42284  hlhilset  42391  dvun  42802  fsuppssindlem2  43036  istopclsd  43143  fzsplit1nn0  43197  diophrw  43202  eldioph2lem1  43203  eldioph2lem2  43204  diophin  43215  diophren  43256  pwssplit4  43532  mendval  43622  iocunico  43654  tfsconcatun  43780  tfsconcat0i  43788  onsucunitp  43816  oaun3  43825  rclexi  44057  rtrclex  44059  rtrclexi  44063  cnvrcl0  44067  dfrtrcl5  44071  dfrcl2  44116  dfrcl3  44117  iunrelexp0  44144  trclfvdecomr  44170  dfrtrcl4  44180  frege131d  44206  clsk3nimkb  44482  clsk1indlem3  44485  clsk1independent  44488  ntrclskb  44511  ntrclsk3  44512  ntrclsk13  44513  permaxinf2lem  45454  dvmptfprodlem  46387  caratheodorylem1  46969  ovnsubadd2lem  47088  ovolval4lem1  47092  fzopredsuc  47769  clnbgrval  48295  cycl3grtri  48420  aacllem  50273