Theorem uneq12d 4123

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

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

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 3444  df-un 3908

This theorem is referenced by:  symdifeq1  4209  csbun  4395  csbprg  4668  disjpr2  4672  diftpsn3  4760  iunxprg  5053  relresdm1  6000  rnpropg  6188  suceqd  6392  fntpg  6560  foun  6800  f1oprswap  6827  fnimapr  6925  fnimatpd  6926  xpprsng  7095  residpr  7098  fvsnun2  7139  fsnunfv  7143  fsnunres  7144  f1ounsn  7228  f1ofvswap  7262  xpord2pred  8097  xpord3pred  8104  frrlem12  8249  oarec  8499  ereq1  8653  mapunen  9086  cnfcomlem  9620  trcl  9649  djueq12  9828  r0weon  9934  infxpen  9936  cfsmolem  10192  cfsmo  10193  axdc3lem4  10375  ttukeylem3  10433  ttukey2g  10438  alephadd  10500  fpwwe2lem12  10565  wunex2  10661  wuncval2  10670  inar1  10698  prunioo  13409  fztp  13508  fzsuc2  13510  fseq1p1m1  13526  s3tpop  14844  s4dom  14854  s2rn  14898  s3rn  14899  s7rn  14900  trclun  14949  relexp0g  14957  relexpsucnnr  14960  dfrtrcl2  14997  setsvalg  17105  setsdm  17109  setsfun0  17111  setsid  17146  prdsval  17387  imasval  17444  mreexd  17577  mreexexlemd  17579  estrreslem2  18073  ipoval  18465  istsr  18518  mndpsuppss  18702  gsumzaddlem  19862  pwssplit1  21023  psrval  21883  psdmullem  22120  ordtval  23145  ordtcnv  23157  paste  23250  connsuba  23376  ptval2  23557  dfac14  23574  xkoptsub  23610  ptuncnv  23763  ptunhmeo  23764  xpstopnlem1  23765  alexsubALTlem3  24005  ustuqtop1  24197  rrxmvallem  25372  ovolioo  25537  uniiccdif  25547  itgsplitioo  25807  limcfval  25841  lhop2  25988  lgsquadlem2  27360  nodenselem5  27668  nosupbnd2lem1  27695  nosupbnd2  27696  noinfbnd2lem1  27710  noinfbnd2  27711  noetainflem2  27718  madeoldsuc  27893  lrold  27905  lrrecval  27947  addsval  27970  addsrid  27972  addscom  27974  addsproplem1  27977  addsprop  27984  addsass  28013  mulsval  28117  mulsrid  28121  mulsproplemcbv  28123  mulsproplem1  28124  mulsprop  28138  mulscom  28147  addsdi  28163  mulsass  28174  mulsunif2lem  28177  precsexlemcbv  28214  precsexlem3  28217  n0cut  28342  halfcut  28466  pw2cut2  28470  readdscl  28507  remulscl  28510  axlowdimlem13  29039  axlowdimlem15  29041  axlowdim  29046  eengv  29064  vtxdun  29567  trlsegvdeg  30314  numclwwlk3lem2lem  30470  ex-res  30528  imadifxp  32687  fresunsn  32714  suppun2  32773  cnvprop  32785  mptprop  32787  coprprop  32788  fmptunsnop  32789  padct  32807  resf1o  32819  symgcom  33176  tocycfv  33202  tocycf  33210  tocyc01  33211  cycpm2tr  33212  cycpmco2f1  33217  cycpmco2rn  33218  cycpmconjv  33235  cycpmconjslem2  33248  elrgspnlem4  33338  rlocval  33352  idlsrgval  33595  rprmval  33608  extvfvcl  33712  zarclsun  34047  ordtprsval  34095  ordtprsuni  34096  ordtcnvNEW  34097  unelcarsg  34489  carsgclctunlem1  34494  eulerpartlemt  34548  sseqval  34565  probun  34596  bnj1373  35205  bnj1489  35231  cvmliftlem10  35507  satfvsuc  35574  satfdm  35582  satf0suc  35589  sat1el2xp  35592  fmlasuc0  35597  satffunlem1lem1  35615  satffunlem2lem1  35617  mrexval  35714  mrsubffval  35720  msrval  35751  mthmpps  35795  lineunray  36360  rdgssun  37630  exrecfnlem  37631  finixpnum  37853  ptrest  37867  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem5  37873  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem9  37877  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem18  37886  poimirlem19  37887  poimirlem20  37888  poimirlem21  37889  poimirlem22  37890  poimirlem23  37891  poimirlem24  37892  poimirlem26  37894  poimirlem27  37895  poimirlem28  37896  poimirlem32  37900  mblfinlem2  37906  itg2addnclem2  37920  ecun  38641  ecuncnvepres  38643  ldualset  39498  paddval  40171  paddcom  40186  dvafset  41377  dvaset  41378  dvhfset  41453  dvhset  41454  hdmapfval  42200  hlhilset  42307  dvun  42726  fsuppssindlem2  42947  istopclsd  43054  fzsplit1nn0  43108  diophrw  43113  eldioph2lem1  43114  eldioph2lem2  43115  diophin  43126  diophren  43167  pwssplit4  43443  mendval  43533  iocunico  43565  tfsconcatun  43691  tfsconcat0i  43699  onsucunitp  43727  oaun3  43736  rclexi  43968  rtrclex  43970  rtrclexi  43974  cnvrcl0  43978  dfrtrcl5  43982  dfrcl2  44027  dfrcl3  44028  iunrelexp0  44055  trclfvdecomr  44081  dfrtrcl4  44091  frege131d  44117  clsk3nimkb  44393  clsk1indlem3  44396  clsk1independent  44399  ntrclskb  44422  ntrclsk3  44423  ntrclsk13  44424  permaxinf2lem  45365  dvmptfprodlem  46299  caratheodorylem1  46881  ovnsubadd2lem  47000  ovolval4lem1  47004  fzopredsuc  47680  clnbgrval  48179  cycl3grtri  48304  aacllem  50157