Theorem uneq12d 4116

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  symdifeq1  4201  csbun  4399  csbprg  4670  disjpr2  4674  diftpsn3  4765  iunxprg  5056  relresdm1  6027  rnpropg  6216  suceqd  6423  fntpg  6592  foun  6835  f1oprswap  6862  fnimapr  6960  fnimatpd  6961  xpprsng  7134  xpsnprg  7135  xpsntpg  7136  residpr  7138  fvsnun2  7180  fsnunfv  7184  fsnunres  7185  f1ounsn  7272  f1ofvswap  7306  xpord2pred  8146  xpord3pred  8153  frrlem12  8299  oarec  8554  ereq1  8709  mapunen  9149  cnfcomlem  9684  trcl  9713  djueq12  9966  r0weon  10072  infxpen  10074  cfsmolem  10329  cfsmo  10330  axdc3lem4  10512  ttukeylem3  10570  ttukey2g  10575  alephadd  10643  fpwwe2lem12  10708  wunex2  10804  wuncval2  10813  inar1  10841  prunioo  13593  fztp  13694  fzsuc2  13696  fseq1p1m1  13712  s3tpop  15040  s4dom  15050  s2rn  15096  s3rn  15097  s7rn  15098  trclun  15147  relexp0g  15155  relexpsucnnr  15158  dfrtrcl2  15195  setsvalg  17324  setsdm  17328  setsfun0  17330  setsid  17365  prdsval  17606  imasval  17663  mreexd  17796  mreexexlemd  17798  estrreslem2  18292  ipoval  18684  istsr  18737  mndpsuppss  18939  gsumzaddlem  20115  pwssplit1  21314  psrval  22203  psdmullem  22466  ordtval  23487  ordtcnv  23499  paste  23592  connsuba  23718  ptval2  23900  dfac14  23917  xkoptsub  23953  ptuncnv  24106  ptunhmeo  24107  xpstopnlem1  24108  alexsubALTlem3  24348  ustuqtop1  24540  rrxmvallem  25705  ovolioo  25869  uniiccdif  25879  itgsplitioo  26138  limcfval  26172  lhop2  26315  lgsquadlem2  27690  nodenselem5  28027  nosupbnd2lem1  28054  nosupbnd2  28055  noinfbnd2lem1  28069  noinfbnd2  28070  noetainflem2  28077  madeoldsuc  28253  lrold  28265  lrrecval  28307  addsval  28330  addsrid  28332  addscom  28334  addsproplem1  28337  addsprop  28344  addsass  28373  mulsval  28477  mulsrid  28481  mulsproplemcbv  28483  mulsproplem1  28484  mulsprop  28498  mulscom  28507  addsdi  28523  mulsass  28534  mulsunif2lem  28537  precsexlemcbv  28574  precsexlem3  28577  n0cut  28702  halfcut  28826  pw2cut2  28830  readdscl  28867  remulscl  28870  axlowdimlem13  29514  axlowdimlem15  29516  axlowdim  29521  eengv  29539  vtxdun  30044  trlsegvdeg  30810  numclwwlk3lem2lem  30966  ex-res  31024  imadifxp  33177  fresunsn  33201  suppun2  33259  cnvprop  33271  mptprop  33273  coprprop  33274  fmptunsnop  33275  padct  33292  resf1o  33304  symgcom  33626  tocycfv  33652  tocycf  33660  tocyc01  33661  cycpm2tr  33662  cycpmco2f1  33667  cycpmco2rn  33668  cycpmconjv  33685  cycpmconjslem2  33698  elrgspnlem4  33788  rlocval  33802  idlsrgval  34017  rprmval  34030  extvfvcl  34150  zarclsun  34484  ordtprsval  34532  ordtprsuni  34533  ordtcnvNEW  34534  unelcarsg  34927  carsgclctunlem1  34932  eulerpartlemt  34986  sseqval  35003  probun  35034  bnj1373  35643  bnj1489  35669  cvmliftlem10  36028  satfvsuc  36095  satfdm  36103  satf0suc  36110  sat1el2xp  36113  fmlasuc0  36118  satffunlem1lem1  36136  satffunlem2lem1  36138  mrexval  36235  mrsubffval  36241  msrval  36272  mthmpps  36316  lineunray  36882  rdgssun  38269  exrecfnlem  38270  finixpnum  38496  ptrest  38505  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem9  38515  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  poimirlem32  38538  mblfinlem2  38544  itg2addnclem2  38558  ecun  39293  ecuncnvepres  39295  ldualset  40150  paddval  40823  paddcom  40838  dvafset  42029  dvaset  42030  dvhfset  42105  dvhset  42106  hdmapfval  42852  hlhilset  42959  dvun  43378  fsuppssindlem2  43582  istopclsd  43664  fzsplit1nn0  43718  diophrw  43723  eldioph2lem1  43724  eldioph2lem2  43725  diophin  43736  diophren  43773  pwssplit4  44049  mendval  44139  iocunico  44171  tfsconcatun  44297  tfsconcat0i  44305  onsucunitp  44333  oaun3  44342  rclexi  44574  rtrclex  44576  rtrclexi  44580  cnvrcl0  44584  dfrtrcl5  44588  dfrcl2  44633  dfrcl3  44634  iunrelexp0  44661  trclfvdecomr  44687  dfrtrcl4  44697  frege131d  44723  clsk3nimkb  44999  clsk1indlem3  45002  clsk1independent  45005  ntrclskb  45028  ntrclsk3  45029  ntrclsk13  45030  permaxinf2lem  45954  dvmptfprodlem  46898  caratheodorylem1  47480  ovnsubadd2lem  47599  ovolval4lem1  47603  fzopredsuc  48338  clnbgrval  48864  cycl3grtri  48989  aacllem  50883