Theorem difeq1d 4049

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

Syntax hints:   → wi 4   = wceq 1538   ∖ cdif 3878

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-dif 3884

This theorem is referenced by:  difeq12d  4051  dffv2  6733  phplem4  8683  unfilem3  8768  marypha1lem  8881  infdifsn  9104  cantnfp1lem3  9127  en2other2  9420  isacn  9455  fin23lem28  9751  enfin1ai  9795  fin1a2lem7  9817  fzdifsuc  12962  axdc4uz  13347  leiso  13813  cshimadifsn  14182  isstruct2  16485  setsfun0  16511  strle1  16584  pltfval  17561  f1omvdco2  18568  symgsssg  18587  symgfisg  18588  symggen  18590  pmtrdifellem3  18598  pmtrdifwrdellem3  18603  pmtrdifwrdel2lem1  18604  pmtrdifwrdel  18605  pmtrdifwrdel2  18606  psgnunilem1  18613  psgnunilem5  18614  psgnunilem2  18615  psgnunilem3  18616  gsumval3  19020  dmdprd  19113  dprd2da  19157  dmdprdsplit2lem  19160  dpjfval  19170  ablfac1eulem  19187  subdrgint  19575  lssset  19698  lbspropd  19864  islindf  20501  islindf2  20503  f1lindf  20511  opsrtoslem2  20724  cldval  21628  difopn  21639  mretopd  21697  restcld  21777  ordtcld1  21802  ordtcld2  21803  cnclima  21873  iscncl  21874  isreg2  21982  llycmpkgen2  22155  1stckgen  22159  ptval  22175  txcld  22208  ptcld  22218  txkgen  22257  qtopcld  22318  qtoprest  22322  qtopcmap  22324  kqcldsat  22338  regr1lem  22344  trufil  22515  ufildr  22536  opnsubg  22713  cldsubg  22716  blcld  23112  lebnumlem1  23566  bcthlem1  23928  bcth  23933  bcth3  23935  difmbl  24147  itg1val  24287  itgioo  24419  limciun  24497  dvfval  24500  istrkgl  26252  ishpg  26553  eengv  26773  elntg  26778  isuhgr  26853  isushgr  26854  uhgreq12g  26858  isuhgrop  26863  uhgr0vb  26865  uhgrun  26867  uhgrstrrepe  26871  isupgr  26877  upgrop  26887  isumgr  26888  upgrun  26911  isuspgr  26945  isusgr  26946  isuspgrop  26954  nb3grprlem2  27171  uvtxval  27177  nbupgruvtxres  27197  cplgrop  27227  cusgrexi  27233  structtocusgr  27236  1loopgrnb0  27292  isconngr1  27975  frgr3v  28060  difuncomp  30317  imadifxp  30364  fressupp  30448  supppreima  30451  gtiso  30460  difico  30532  fzdif2  30540  fzodif2  30541  fzodif1  30542  pmtrcnel2  30784  cycpmconjvlem  30833  cycpmrn  30835  tocyccntz  30836  submarchi  30865  elrspunidl  31014  qtophaus  31189  imambfm  31630  difelcarsg  31678  carsgclctunlem1  31685  carsggect  31686  issibf  31701  sibf0  31702  sitgfval  31709  ballotlemfval  31857  ballotlemfp1  31859  ballotlemgun  31892  hgt750lemb  32037  kur14  32576  iscvm  32619  cvmscld  32633  satf  32713  mdvval  32864  topbnd  33785  pibp21  34832  poimirlem2  35059  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem16  35073  poimirlem18  35075  poimirlem19  35076  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem27  35084  poimirlem30  35087  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem  35108  itg2addnclem2  35109  prjspeclsp  39606  aomclem8  40005  kelac2  40009  gneispace2  40835  fzdifsuc2  41942  iccdifioo  42152  iccdifprioo  42153  ibliooicc  42613  dirkercncflem2  42746  issal  42956  prsal  42960  saldifcl2  42968  intsal  42970  sge0fodjrnlem  43055  caratheodorylem1  43165  vonvolmbllem  43299  salpreimagelt  43343  salpreimalegt  43345  smfresal  43420  lines  45145  rrxlines  45147  eenglngeehlnm  45153