Theorem uneq2d 4109

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 4103	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	syl 17	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:  ifeq2  4472  tpeq3  4689  iununi  5042  sucprc  6396  unisucs  6397  resasplit  6705  fvun1  6926  fmptapd  7120  fndifnfp  7125  fvunsn  7128  fnsnsplit  7133  f1ofvswap  7255  oev2  8452  oarec  8491  ralxpmap  8838  sbthlem5  9023  sbthlem6  9024  domss2  9068  dif1en  9090  unfi  9099  fodomfi  9216  domunfican  9226  fiint  9231  fodomfiOLD  9234  pm54.43  9919  kmlem2  10068  kmlem11  10077  ackbij1lem1  10135  fin23lem26  10241  axdc3lem4  10369  fpwwe2lem12  10559  wunex2  10655  wuncval2  10664  indconst1  12166  ioounsn  13424  snunico  13426  ioojoin  13430  fzsuc  13519  fseq1p1m1  13546  fseq1m1p1  13547  fzosplitsnm1  13689  fzosplitsn  13725  fzosplitpr  13726  fzosplitprm1  13727  hashfun  14393  resunimafz0  14401  s4prop  14866  fsumm1  15707  climcndslem1  15808  fprodm1  15926  ruclem4  16195  lcmfunsnlem1  16600  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  lcmfunsnlem2  16603  lcmfunsn  16607  vdwap1  16942  setscom  17144  setsidvald  17163  mreexmrid  17603  mreexexlemd  17604  mreexexlem2d  17605  cnvtsr  18548  dprd2da  20013  dmdprdsplit2lem  20016  lspun0  21000  lbsextlem4  21154  cmpcld  23380  comppfsc  23510  trfil2  23865  cldsubg  24089  tsmsres  24122  icccmplem2  24802  uniioombllem4  25566  ppiprm  27131  chtprm  27133  pntrsumbnd2  27547  noextend  27647  nodenselem5  27669  nosupbnd2lem1  27696  addsproplem1  27978  addsprop  27985  negsproplem1  28037  negsprop  28044  mulsproplemcbv  28124  mulsproplem1  28125  mulsprop  28139  precsexlemcbv  28215  precsexlem3  28218  onleft  28269  ltonold  28270  oncutlt  28273  pthdlem1  29852  wwlksnext  29979  clwwlknonex2lem1  30195  iunxunsn  32654  iunxunpr  32655  difres  32688  ofpreima2  32757  fzspl  32880  tocyc01  33197  esplyind  33737  ordtprsuni  34082  ordtcnvNEW  34083  carsgsigalem  34478  ballotlemfp1  34655  fsum2dsub  34770  reprsuc  34778  bnj941  34934  bnj944  35099  fineqvac  35279  subfacp1lem1  35380  cvmscld  35474  satf  35554  satfv1  35564  fmlasuc  35587  mrsubvrs  35723  mclsval  35764  rankaltopb  36180  rankung  36367  lindsadd  37951  lindsenlbs  37953  poimirlem1  37959  poimirlem2  37960  poimirlem4  37962  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem13  37971  poimirlem14  37972  poimirlem16  37974  poimirlem17  37975  poimirlem18  37976  poimirlem19  37977  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem26  37984  poimirlem28  37986  poimirlem31  37989  poimirlem32  37990  lshpnel2N  39448  paddfval  40260  hdmapval  42291  fzsplitnd  42438  lcmfunnnd  42468  fsuppssind  43043  diophren  43262  omabs2  43781  tfsconcatrn  43791  tfsconcatrev  43797  iunrelexp0  44150  trclfvdecoml  44177  isotone1  44496  iunp1  45518  snunioo1  45963  dvmptfprodlem  46393  stoweidlem11  46460  stoweidlem26  46475  fourierdlem33  46589  fzopredsuc  47787  iccpartltu  47900  iccpartgt  47902  dfclnbgr2  48314  dfclnbgr4  48315  dfclnbgr3  48317  clnbupgr  48324  clnbgr0edg  48328  dfclnbgr5  48341  dfclnbgr6  48347  dfsclnbgr6  48349  cycl3grtri  48438  stgrclnbgr0  48456  lmod1zr  48984  tposres2  49370