Theorem difeq1d 4065

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 4059	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3886

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-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  difeq12d  4067  dffv2  6935  on2recsov  8604  phplem2  9139  unfilem3  9217  marypha1lem  9346  infdifsn  9578  cantnfp1lem3  9601  en2other2  9931  isacn  9966  fin23lem28  10262  enfin1ai  10306  fin1a2lem7  10328  fzdifsuc  13538  axdc4uz  13946  leiso  14421  cshimadifsn  14791  isstruct2  17119  strle1  17128  setsfun0  17142  pltfval  18295  ischn  18573  chnind  18587  chnccats1  18591  chnccat  18592  f1omvdco2  19423  symgsssg  19442  symgfisg  19443  symggen  19445  pmtrdifellem3  19453  pmtrdifwrdellem3  19458  pmtrdifwrdel2lem1  19459  pmtrdifwrdel  19460  pmtrdifwrdel2  19461  psgnunilem1  19468  psgnunilem5  19469  psgnunilem2  19470  psgnunilem3  19471  gsumval3  19882  dmdprd  19975  dprd2da  20019  dmdprdsplit2lem  20022  dpjfval  20032  ablfac1eulem  20049  subdrgint  20780  lssset  20928  lbspropd  21094  islindf  21792  islindf2  21794  f1lindf  21802  opsrtoslem2  22034  cldval  22988  difopn  22999  mretopd  23057  restcld  23137  ordtcld1  23162  ordtcld2  23163  cnclima  23233  iscncl  23234  isreg2  23342  llycmpkgen2  23515  1stckgen  23519  ptval  23535  txcld  23568  ptcld  23578  txkgen  23617  qtopcld  23678  qtoprest  23682  qtopcmap  23684  kqcldsat  23698  regr1lem  23704  trufil  23875  ufildr  23896  opnsubg  24073  cldsubg  24076  blcld  24470  lebnumlem1  24928  bcthlem1  25291  bcth  25296  bcth3  25298  difmbl  25510  itg1val  25650  itgioo  25783  limciun  25861  dvfval  25864  newval  27827  noxpordpred  27945  istrkgl  28526  ishpg  28827  eengv  29048  elntg  29053  isuhgr  29129  isushgr  29130  uhgreq12g  29134  isuhgrop  29139  uhgr0vb  29141  uhgrun  29143  uhgrstrrepe  29147  isupgr  29153  upgrop  29163  isumgr  29164  upgrun  29187  isuspgr  29221  isusgr  29222  isuspgrop  29230  nb3grprlem2  29450  uvtxval  29456  nbupgruvtxres  29476  cplgrop  29506  cusgrexi  29512  structtocusgr  29515  1loopgrnb0  29571  cyclnumvtx  29868  isconngr1  30260  frgr3v  30345  difuncomp  32623  imadifxp  32671  fresunsn  32698  fressupp  32761  supppreima  32764  mptiffisupp  32766  gtiso  32774  difico  32856  fzdif2  32863  fzodif2  32864  fzodif1  32865  nn0diffz0  32867  pmtrcnel2  33151  cycpmconjvlem  33202  cycpmrn  33204  tocyccntz  33205  submarchi  33247  elrgspnlem4  33306  fracfld  33369  elrspunidl  33488  psrbasfsupp  33672  qtophaus  33980  imambfm  34406  difelcarsg  34454  carsgclctunlem1  34461  carsggect  34462  issibf  34477  sibf0  34478  sitgfval  34485  ballotlemfval  34634  ballotlemfp1  34636  ballotlemgun  34669  hgt750lemb  34800  kur14  35398  iscvm  35441  cvmscld  35455  satf  35535  mdvval  35686  topbnd  36506  pibp21  37731  poimirlem2  37943  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem18  37959  poimirlem19  37960  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem27  37968  poimirlem30  37971  mblfinlem3  37980  mblfinlem4  37981  itg2addnclem  37992  itg2addnclem2  37993  prjspeclsp  43045  aomclem8  43489  kelac2  43493  gneispace2  44559  fzdifsuc2  45743  iccdifioo  45945  iccdifprioo  45946  ibliooicc  46399  dirkercncflem2  46532  issal  46742  prsal  46746  saldifcl2  46756  intsal  46758  sge0fodjrnlem  46844  caratheodorylem1  46954  vonvolmbllem  47088  salpreimagelt  47135  salpreimalegt  47137  smfresal  47216  chnsubseq  47310  dfnbgr5  48327  dfnbgr6  48333  isubgruhgr  48344  stgrnbgr0  48440  lines  49207  rrxlines  49209  eenglngeehlnm  49215  clddisj  49379  iscnrm3rlem1  49415