Theorem uneq2d 4108

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
uneq2d	⊢ (𝜑 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq2 4102	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 17	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:  ifeq2  4471  tpeq3  4688  iununi  5041  sucprc  6401  unisucs  6402  resasplit  6710  fvun1  6931  fmptapd  7126  fndifnfp  7131  fvunsn  7134  fnsnsplit  7139  f1ofvswap  7261  oev2  8458  oarec  8497  ralxpmap  8844  sbthlem5  9029  sbthlem6  9030  domss2  9074  dif1en  9096  unfi  9105  fodomfi  9222  domunfican  9232  fiint  9237  fodomfiOLD  9240  pm54.43  9925  kmlem2  10074  kmlem11  10083  ackbij1lem1  10141  fin23lem26  10247  axdc3lem4  10375  fpwwe2lem12  10565  wunex2  10661  wuncval2  10670  indconst1  12172  ioounsn  13430  snunico  13432  ioojoin  13436  fzsuc  13525  fseq1p1m1  13552  fseq1m1p1  13553  fzosplitsnm1  13695  fzosplitsn  13731  fzosplitpr  13732  fzosplitprm1  13733  hashfun  14399  resunimafz0  14407  s4prop  14872  fsumm1  15713  climcndslem1  15814  fprodm1  15932  ruclem4  16201  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  lcmfunsn  16613  vdwap1  16948  setscom  17150  setsidvald  17169  mreexmrid  17609  mreexexlemd  17610  mreexexlem2d  17611  cnvtsr  18554  dprd2da  20019  dmdprdsplit2lem  20022  lspun0  21006  lbsextlem4  21159  cmpcld  23367  comppfsc  23497  trfil2  23852  cldsubg  24076  tsmsres  24109  icccmplem2  24789  uniioombllem4  25553  ppiprm  27114  chtprm  27116  pntrsumbnd2  27530  noextend  27630  nodenselem5  27652  nosupbnd2lem1  27679  addsproplem1  27961  addsprop  27968  negsproplem1  28020  negsprop  28027  mulsproplemcbv  28107  mulsproplem1  28108  mulsprop  28122  precsexlemcbv  28198  precsexlem3  28201  onleft  28252  ltonold  28253  oncutlt  28256  pthdlem1  29834  wwlksnext  29961  clwwlknonex2lem1  30177  iunxunsn  32636  iunxunpr  32637  difres  32670  ofpreima2  32739  fzspl  32862  tocyc01  33179  esplyind  33719  ordtprsuni  34063  ordtcnvNEW  34064  carsgsigalem  34459  ballotlemfp1  34636  fsum2dsub  34751  reprsuc  34759  bnj941  34915  bnj944  35080  fineqvac  35260  subfacp1lem1  35361  cvmscld  35455  satf  35535  satfv1  35545  fmlasuc  35568  mrsubvrs  35704  mclsval  35745  rankaltopb  36161  rankung  36348  lindsadd  37934  lindsenlbs  37936  poimirlem1  37942  poimirlem2  37943  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem26  37967  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  lshpnel2N  39431  paddfval  40243  hdmapval  42274  fzsplitnd  42421  lcmfunnnd  42451  fsuppssind  43026  diophren  43241  omabs2  43760  tfsconcatrn  43770  tfsconcatrev  43776  iunrelexp0  44129  trclfvdecoml  44156  isotone1  44475  iunp1  45497  snunioo1  45942  dvmptfprodlem  46372  stoweidlem11  46439  stoweidlem26  46454  fourierdlem33  46568  fzopredsuc  47772  iccpartltu  47885  iccpartgt  47887  dfclnbgr2  48299  dfclnbgr4  48300  dfclnbgr3  48302  clnbupgr  48309  clnbgr0edg  48313  dfclnbgr5  48326  dfclnbgr6  48332  dfsclnbgr6  48334  cycl3grtri  48423  stgrclnbgr0  48441  lmod1zr  48969  tposres2  49355