Theorem uneq12d 4091

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

Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3879

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  symdifeq1  4171  csbun  4346  csbprg  4605  disjpr2  4609  diftpsn3  4695  iunxprg  4981  rnpropg  6046  suceq  6224  fntpg  6384  foun  6608  f1oprswap  6633  fnimapr  6722  xpprsng  6879  residpr  6882  fvsnun2  6922  fsnunfv  6926  fsnunres  6927  oarec  8171  ereq1  8279  mapunen  8670  cnfcomlem  9146  trcl  9154  djueq12  9317  r0weon  9423  infxpen  9425  cfsmolem  9681  cfsmo  9682  axdc3lem4  9864  ttukeylem3  9922  ttukey2g  9927  alephadd  9988  fpwwe2lem13  10053  wunex2  10149  wuncval2  10158  inar1  10186  prunioo  12859  fztp  12958  fzsuc2  12960  fseq1p1m1  12976  s3tpop  14262  s4dom  14272  trclun  14365  relexp0g  14373  relexpsucnnr  14376  dfrtrcl2  14413  setsvalg  16504  setsdm  16509  setsfun0  16511  setsid  16530  prdsval  16720  imasval  16776  mreexd  16905  mreexexlemd  16907  estrreslem2  17380  ipoval  17756  istsr  17819  gsumzaddlem  19034  pwssplit1  19824  psrval  20600  ordtval  21794  ordtcnv  21806  paste  21899  connsuba  22025  ptval2  22206  dfac14  22223  xkoptsub  22259  ptuncnv  22412  ptunhmeo  22413  xpstopnlem1  22414  alexsubALTlem3  22654  ustuqtop1  22847  rrxmvallem  24008  ovolioo  24172  uniiccdif  24182  itgsplitioo  24441  limcfval  24475  lhop2  24618  lgsquadlem2  25965  axlowdimlem13  26748  axlowdimlem15  26750  axlowdim  26755  eengv  26773  vtxdun  27271  trlsegvdeg  28012  numclwwlk3lem2lem  28168  ex-res  28226  imadifxp  30364  funresdm1  30368  fnimatp  30440  cnvprop  30456  mptprop  30458  coprprop  30459  padct  30481  resf1o  30492  symgcom  30777  tocycfv  30801  tocycf  30809  tocyc01  30810  cycpm2tr  30811  cycpmco2f1  30816  cycpmco2rn  30817  cycpmconjv  30834  cycpmconjslem2  30847  idlsrgval  31056  rprmval  31072  zarclsun  31223  ordtprsval  31271  ordtprsuni  31272  ordtcnvNEW  31273  unelcarsg  31680  carsgclctunlem1  31685  eulerpartlemt  31739  sseqval  31756  probun  31787  bnj1373  32412  bnj1489  32438  cvmliftlem10  32654  satfvsuc  32721  satfdm  32729  satf0suc  32736  sat1el2xp  32739  fmlasuc0  32744  satffunlem1lem1  32762  satffunlem2lem1  32764  mrexval  32861  mrsubffval  32867  msrval  32898  mthmpps  32942  frrlem12  33247  nodenselem5  33305  nosupbnd2lem1  33328  nosupbnd2  33329  lineunray  33721  rdgssun  34795  exrecfnlem  34796  finixpnum  35042  ptrest  35056  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  poimirlem32  35089  mblfinlem2  35095  itg2addnclem2  35109  ldualset  36421  paddval  37094  paddcom  37109  dvafset  38300  dvaset  38301  dvhfset  38376  dvhset  38377  hdmapfval  39123  hlhilset  39230  metakunt17  39366  metakunt20  39369  metakunt21  39370  metakunt22  39371  metakunt24  39373  fsuppssindlem2  39458  istopclsd  39641  fzsplit1nn0  39695  diophrw  39700  eldioph2lem1  39701  eldioph2lem2  39702  diophin  39713  diophren  39754  pwssplit4  40033  mendval  40127  iocunico  40161  rclexi  40315  rtrclex  40317  rtrclexi  40321  cnvrcl0  40325  dfrtrcl5  40329  dfrcl2  40375  dfrcl3  40376  iunrelexp0  40403  trclfvdecomr  40429  dfrtrcl4  40439  frege131d  40465  clsk3nimkb  40743  clsk1indlem3  40746  clsk1independent  40749  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  dvmptfprodlem  42586  caratheodorylem1  43165  ovnsubadd2lem  43284  ovolval4lem1  43288  fzopredsuc  43880  mndpsuppss  44773  aacllem  45329