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  5992  rnpropg  6180  suceqd  6384  fntpg  6552  foun  6792  f1oprswap  6819  fnimapr  6917  fnimatpd  6918  xpprsng  7087  residpr  7090  fvsnun2  7131  fsnunfv  7135  fsnunres  7136  f1ounsn  7220  f1ofvswap  7254  xpord2pred  8088  xpord3pred  8095  frrlem12  8240  oarec  8490  ereq1  8644  mapunen  9077  cnfcomlem  9611  trcl  9640  djueq12  9819  r0weon  9925  infxpen  9927  cfsmolem  10183  cfsmo  10184  axdc3lem4  10366  ttukeylem3  10424  ttukey2g  10429  alephadd  10491  fpwwe2lem12  10556  wunex2  10652  wuncval2  10661  inar1  10689  prunioo  13425  fztp  13525  fzsuc2  13527  fseq1p1m1  13543  s3tpop  14862  s4dom  14872  s2rn  14916  s3rn  14917  s7rn  14918  trclun  14967  relexp0g  14975  relexpsucnnr  14978  dfrtrcl2  15015  setsvalg  17127  setsdm  17131  setsfun0  17133  setsid  17168  prdsval  17409  imasval  17466  mreexd  17599  mreexexlemd  17601  estrreslem2  18095  ipoval  18487  istsr  18540  mndpsuppss  18724  gsumzaddlem  19887  pwssplit1  21046  psrval  21905  psdmullem  22141  ordtval  23164  ordtcnv  23176  paste  23269  connsuba  23395  ptval2  23576  dfac14  23593  xkoptsub  23629  ptuncnv  23782  ptunhmeo  23783  xpstopnlem1  23784  alexsubALTlem3  24024  ustuqtop1  24216  rrxmvallem  25381  ovolioo  25545  uniiccdif  25555  itgsplitioo  25815  limcfval  25849  lhop2  25992  lgsquadlem2  27358  nodenselem5  27666  nosupbnd2lem1  27693  nosupbnd2  27694  noinfbnd2lem1  27708  noinfbnd2  27709  noetainflem2  27716  madeoldsuc  27891  lrold  27903  lrrecval  27945  addsval  27968  addsrid  27970  addscom  27972  addsproplem1  27975  addsprop  27982  addsass  28011  mulsval  28115  mulsrid  28119  mulsproplemcbv  28121  mulsproplem1  28122  mulsprop  28136  mulscom  28145  addsdi  28161  mulsass  28172  mulsunif2lem  28175  precsexlemcbv  28212  precsexlem3  28215  n0cut  28340  halfcut  28464  pw2cut2  28468  readdscl  28505  remulscl  28508  axlowdimlem13  29037  axlowdimlem15  29039  axlowdim  29044  eengv  29062  vtxdun  29565  trlsegvdeg  30312  numclwwlk3lem2lem  30468  ex-res  30526  imadifxp  32686  fresunsn  32713  suppun2  32772  cnvprop  32784  mptprop  32786  coprprop  32787  fmptunsnop  32788  padct  32806  resf1o  32818  symgcom  33159  tocycfv  33185  tocycf  33193  tocyc01  33194  cycpm2tr  33195  cycpmco2f1  33200  cycpmco2rn  33201  cycpmconjv  33218  cycpmconjslem2  33231  elrgspnlem4  33321  rlocval  33335  idlsrgval  33578  rprmval  33591  extvfvcl  33695  zarclsun  34030  ordtprsval  34078  ordtprsuni  34079  ordtcnvNEW  34080  unelcarsg  34472  carsgclctunlem1  34477  eulerpartlemt  34531  sseqval  34548  probun  34579  bnj1373  35188  bnj1489  35214  cvmliftlem10  35492  satfvsuc  35559  satfdm  35567  satf0suc  35574  sat1el2xp  35577  fmlasuc0  35582  satffunlem1lem1  35600  satffunlem2lem1  35602  mrexval  35699  mrsubffval  35705  msrval  35736  mthmpps  35780  lineunray  36345  rdgssun  37708  exrecfnlem  37709  finixpnum  37940  ptrest  37954  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem9  37964  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem32  37987  mblfinlem2  37993  itg2addnclem2  38007  ecun  38728  ecuncnvepres  38730  ldualset  39585  paddval  40258  paddcom  40273  dvafset  41464  dvaset  41465  dvhfset  41540  dvhset  41541  hdmapfval  42287  hlhilset  42394  dvun  42805  fsuppssindlem2  43039  istopclsd  43146  fzsplit1nn0  43200  diophrw  43205  eldioph2lem1  43206  eldioph2lem2  43207  diophin  43218  diophren  43259  pwssplit4  43535  mendval  43625  iocunico  43657  tfsconcatun  43783  tfsconcat0i  43791  onsucunitp  43819  oaun3  43828  rclexi  44060  rtrclex  44062  rtrclexi  44066  cnvrcl0  44070  dfrtrcl5  44074  dfrcl2  44119  dfrcl3  44120  iunrelexp0  44147  trclfvdecomr  44173  dfrtrcl4  44183  frege131d  44209  clsk3nimkb  44485  clsk1indlem3  44488  clsk1independent  44491  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  permaxinf2lem  45457  dvmptfprodlem  46390  caratheodorylem1  46972  ovnsubadd2lem  47091  ovolval4lem1  47095  fzopredsuc  47784  clnbgrval  48310  cycl3grtri  48435  aacllem  50288