Theorem difeq1d 4075

Description: Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

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

Assertion

Ref	Expression
difeq1d	⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Proof of Theorem difeq1d

Step	Hyp	Ref	Expression
1		difeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		difeq1 4069	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-dif 3905

This theorem is referenced by:  difeq12d  4077  dffv2  6917  on2recsov  8583  phplem2  9114  unfilem3  9191  marypha1lem  9317  infdifsn  9547  cantnfp1lem3  9570  en2other2  9900  isacn  9935  fin23lem28  10231  enfin1ai  10275  fin1a2lem7  10297  fzdifsuc  13484  axdc4uz  13891  leiso  14366  cshimadifsn  14736  isstruct2  17060  strle1  17069  setsfun0  17083  pltfval  18235  ischn  18513  chnind  18527  chnccats1  18531  chnccat  18532  f1omvdco2  19361  symgsssg  19380  symgfisg  19381  symggen  19383  pmtrdifellem3  19391  pmtrdifwrdellem3  19396  pmtrdifwrdel2lem1  19397  pmtrdifwrdel  19398  pmtrdifwrdel2  19399  psgnunilem1  19406  psgnunilem5  19407  psgnunilem2  19408  psgnunilem3  19409  gsumval3  19820  dmdprd  19913  dprd2da  19957  dmdprdsplit2lem  19960  dpjfval  19970  ablfac1eulem  19987  subdrgint  20719  lssset  20867  lbspropd  21034  islindf  21750  islindf2  21752  f1lindf  21760  opsrtoslem2  21992  cldval  22939  difopn  22950  mretopd  23008  restcld  23088  ordtcld1  23113  ordtcld2  23114  cnclima  23184  iscncl  23185  isreg2  23293  llycmpkgen2  23466  1stckgen  23470  ptval  23486  txcld  23519  ptcld  23529  txkgen  23568  qtopcld  23629  qtoprest  23633  qtopcmap  23635  kqcldsat  23649  regr1lem  23655  trufil  23826  ufildr  23847  opnsubg  24024  cldsubg  24027  blcld  24421  lebnumlem1  24888  bcthlem1  25252  bcth  25257  bcth3  25259  difmbl  25472  itg1val  25612  itgioo  25745  limciun  25823  dvfval  25826  newval  27797  noxpordpred  27897  istrkgl  28437  ishpg  28738  eengv  28958  elntg  28963  isuhgr  29039  isushgr  29040  uhgreq12g  29044  isuhgrop  29049  uhgr0vb  29051  uhgrun  29053  uhgrstrrepe  29057  isupgr  29063  upgrop  29073  isumgr  29074  upgrun  29097  isuspgr  29131  isusgr  29132  isuspgrop  29140  nb3grprlem2  29360  uvtxval  29366  nbupgruvtxres  29386  cplgrop  29416  cusgrexi  29422  structtocusgr  29425  1loopgrnb0  29482  cyclnumvtx  29779  isconngr1  30168  frgr3v  30253  difuncomp  32531  imadifxp  32579  fressupp  32667  supppreima  32670  mptiffisupp  32672  gtiso  32680  difico  32764  fzdif2  32771  fzodif2  32772  fzodif1  32773  pmtrcnel2  33057  cycpmconjvlem  33108  cycpmrn  33110  tocyccntz  33111  submarchi  33153  elrgspnlem4  33210  fracfld  33272  elrspunidl  33391  psrbasfsupp  33570  qtophaus  33847  imambfm  34273  difelcarsg  34321  carsgclctunlem1  34328  carsggect  34329  issibf  34344  sibf0  34345  sitgfval  34352  ballotlemfval  34501  ballotlemfp1  34503  ballotlemgun  34536  hgt750lemb  34667  kur14  35258  iscvm  35301  cvmscld  35315  satf  35395  mdvval  35546  topbnd  36364  pibp21  37455  poimirlem2  37668  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem11  37677  poimirlem12  37678  poimirlem13  37679  poimirlem14  37680  poimirlem16  37682  poimirlem18  37684  poimirlem19  37685  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem27  37693  poimirlem30  37696  mblfinlem3  37705  mblfinlem4  37706  itg2addnclem  37717  itg2addnclem2  37718  prjspeclsp  42651  aomclem8  43100  kelac2  43104  gneispace2  44171  fzdifsuc2  45357  iccdifioo  45561  iccdifprioo  45562  ibliooicc  46015  dirkercncflem2  46148  issal  46358  prsal  46362  saldifcl2  46372  intsal  46374  sge0fodjrnlem  46460  caratheodorylem1  46570  vonvolmbllem  46704  salpreimagelt  46751  salpreimalegt  46753  smfresal  46832  dfnbgr5  47888  dfnbgr6  47894  isubgruhgr  47905  stgrnbgr0  48001  lines  48769  rrxlines  48771  eenglngeehlnm  48777  clddisj  48941  iscnrm3rlem1  48977