Theorem uneq12d 4109

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  symdifeq1  4195  csbun  4381  csbprg  4653  disjpr2  4657  diftpsn3  4747  iunxprg  5038  relresdm1  5998  rnpropg  6186  suceqd  6390  fntpg  6558  foun  6798  f1oprswap  6825  fnimapr  6923  fnimatpd  6924  xpprsng  7093  residpr  7096  fvsnun2  7138  fsnunfv  7142  fsnunres  7143  f1ounsn  7227  f1ofvswap  7261  xpord2pred  8095  xpord3pred  8102  frrlem12  8247  oarec  8497  ereq1  8651  mapunen  9084  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  13434  fztp  13534  fzsuc2  13536  fseq1p1m1  13552  s3tpop  14871  s4dom  14881  s2rn  14925  s3rn  14926  s7rn  14927  trclun  14976  relexp0g  14984  relexpsucnnr  14987  dfrtrcl2  15024  setsvalg  17136  setsdm  17140  setsfun0  17142  setsid  17177  prdsval  17418  imasval  17475  mreexd  17608  mreexexlemd  17610  estrreslem2  18104  ipoval  18496  istsr  18549  mndpsuppss  18733  gsumzaddlem  19896  pwssplit1  21054  psrval  21895  psdmullem  22131  ordtval  23154  ordtcnv  23166  paste  23259  connsuba  23385  ptval2  23566  dfac14  23583  xkoptsub  23619  ptuncnv  23772  ptunhmeo  23773  xpstopnlem1  23774  alexsubALTlem3  24014  ustuqtop1  24206  rrxmvallem  25371  ovolioo  25535  uniiccdif  25545  itgsplitioo  25805  limcfval  25839  lhop2  25982  lgsquadlem2  27344  nodenselem5  27652  nosupbnd2lem1  27679  nosupbnd2  27680  noinfbnd2lem1  27694  noinfbnd2  27695  noetainflem2  27702  madeoldsuc  27877  lrold  27889  lrrecval  27931  addsval  27954  addsrid  27956  addscom  27958  addsproplem1  27961  addsprop  27968  addsass  27997  mulsval  28101  mulsrid  28105  mulsproplemcbv  28107  mulsproplem1  28108  mulsprop  28122  mulscom  28131  addsdi  28147  mulsass  28158  mulsunif2lem  28161  precsexlemcbv  28198  precsexlem3  28201  n0cut  28326  halfcut  28450  pw2cut2  28454  readdscl  28491  remulscl  28494  axlowdimlem13  29023  axlowdimlem15  29025  axlowdim  29030  eengv  29048  vtxdun  29550  trlsegvdeg  30297  numclwwlk3lem2lem  30453  ex-res  30511  imadifxp  32671  fresunsn  32698  suppun2  32757  cnvprop  32769  mptprop  32771  coprprop  32772  fmptunsnop  32773  padct  32791  resf1o  32803  symgcom  33144  tocycfv  33170  tocycf  33178  tocyc01  33179  cycpm2tr  33180  cycpmco2f1  33185  cycpmco2rn  33186  cycpmconjv  33203  cycpmconjslem2  33216  elrgspnlem4  33306  rlocval  33320  idlsrgval  33563  rprmval  33576  extvfvcl  33680  zarclsun  34014  ordtprsval  34062  ordtprsuni  34063  ordtcnvNEW  34064  unelcarsg  34456  carsgclctunlem1  34461  eulerpartlemt  34515  sseqval  34532  probun  34563  bnj1373  35172  bnj1489  35198  cvmliftlem10  35476  satfvsuc  35543  satfdm  35551  satf0suc  35558  sat1el2xp  35561  fmlasuc0  35566  satffunlem1lem1  35584  satffunlem2lem1  35586  mrexval  35683  mrsubffval  35689  msrval  35720  mthmpps  35764  lineunray  36329  rdgssun  37694  exrecfnlem  37695  finixpnum  37926  ptrest  37940  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem32  37973  mblfinlem2  37979  itg2addnclem2  37993  ecun  38714  ecuncnvepres  38716  ldualset  39571  paddval  40244  paddcom  40259  dvafset  41450  dvaset  41451  dvhfset  41526  dvhset  41527  hdmapfval  42273  hlhilset  42380  dvun  42791  fsuppssindlem2  43025  istopclsd  43132  fzsplit1nn0  43186  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  diophin  43204  diophren  43241  pwssplit4  43517  mendval  43607  iocunico  43639  tfsconcatun  43765  tfsconcat0i  43773  onsucunitp  43801  oaun3  43810  rclexi  44042  rtrclex  44044  rtrclexi  44048  cnvrcl0  44052  dfrtrcl5  44056  dfrcl2  44101  dfrcl3  44102  iunrelexp0  44129  trclfvdecomr  44155  dfrtrcl4  44165  frege131d  44191  clsk3nimkb  44467  clsk1indlem3  44470  clsk1independent  44473  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  permaxinf2lem  45439  dvmptfprodlem  46372  caratheodorylem1  46954  ovnsubadd2lem  47073  ovolval4lem1  47077  fzopredsuc  47772  clnbgrval  48298  cycl3grtri  48423  aacllem  50276