Theorem difeq1d 4125

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-dif 3954

This theorem is referenced by:  difeq12d  4127  dffv2  7004  on2recsov  8706  phplem2  9245  phplem4OLD  9257  unfilem3  9345  marypha1lem  9473  infdifsn  9697  cantnfp1lem3  9720  en2other2  10049  isacn  10084  fin23lem28  10380  enfin1ai  10424  fin1a2lem7  10446  fzdifsuc  13624  axdc4uz  14025  leiso  14498  cshimadifsn  14868  isstruct2  17186  strle1  17195  setsfun0  17209  pltfval  18376  f1omvdco2  19466  symgsssg  19485  symgfisg  19486  symggen  19488  pmtrdifellem3  19496  pmtrdifwrdellem3  19501  pmtrdifwrdel2lem1  19502  pmtrdifwrdel  19503  pmtrdifwrdel2  19504  psgnunilem1  19511  psgnunilem5  19512  psgnunilem2  19513  psgnunilem3  19514  gsumval3  19925  dmdprd  20018  dprd2da  20062  dmdprdsplit2lem  20065  dpjfval  20075  ablfac1eulem  20092  subdrgint  20804  lssset  20931  lbspropd  21098  islindf  21832  islindf2  21834  f1lindf  21842  opsrtoslem2  22080  cldval  23031  difopn  23042  mretopd  23100  restcld  23180  ordtcld1  23205  ordtcld2  23206  cnclima  23276  iscncl  23277  isreg2  23385  llycmpkgen2  23558  1stckgen  23562  ptval  23578  txcld  23611  ptcld  23621  txkgen  23660  qtopcld  23721  qtoprest  23725  qtopcmap  23727  kqcldsat  23741  regr1lem  23747  trufil  23918  ufildr  23939  opnsubg  24116  cldsubg  24119  blcld  24518  lebnumlem1  24993  bcthlem1  25358  bcth  25363  bcth3  25365  difmbl  25578  itg1val  25718  itgioo  25851  limciun  25929  dvfval  25932  newval  27894  noxpordpred  27986  istrkgl  28466  ishpg  28767  eengv  28994  elntg  28999  isuhgr  29077  isushgr  29078  uhgreq12g  29082  isuhgrop  29087  uhgr0vb  29089  uhgrun  29091  uhgrstrrepe  29095  isupgr  29101  upgrop  29111  isumgr  29112  upgrun  29135  isuspgr  29169  isusgr  29170  isuspgrop  29178  nb3grprlem2  29398  uvtxval  29404  nbupgruvtxres  29424  cplgrop  29454  cusgrexi  29460  structtocusgr  29463  1loopgrnb0  29520  cyclnumvtx  29820  isconngr1  30209  frgr3v  30294  difuncomp  32566  imadifxp  32614  fressupp  32697  supppreima  32700  mptiffisupp  32702  gtiso  32710  difico  32785  fzdif2  32792  fzodif2  32793  fzodif1  32794  ischn  32996  chnind  33001  chnccats1  33005  pmtrcnel2  33110  cycpmconjvlem  33161  cycpmrn  33163  tocyccntz  33164  submarchi  33193  elrgspnlem4  33249  fracfld  33310  elrspunidl  33456  qtophaus  33835  imambfm  34264  difelcarsg  34312  carsgclctunlem1  34319  carsggect  34320  issibf  34335  sibf0  34336  sitgfval  34343  ballotlemfval  34492  ballotlemfp1  34494  ballotlemgun  34527  hgt750lemb  34671  kur14  35221  iscvm  35264  cvmscld  35278  satf  35358  mdvval  35509  topbnd  36325  pibp21  37416  poimirlem2  37629  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem16  37643  poimirlem18  37645  poimirlem19  37646  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem27  37654  poimirlem30  37657  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  itg2addnclem2  37679  prjspeclsp  42622  aomclem8  43073  kelac2  43077  gneispace2  44145  fzdifsuc2  45322  iccdifioo  45528  iccdifprioo  45529  ibliooicc  45986  dirkercncflem2  46119  issal  46329  prsal  46333  saldifcl2  46343  intsal  46345  sge0fodjrnlem  46431  caratheodorylem1  46541  vonvolmbllem  46675  salpreimagelt  46722  salpreimalegt  46724  smfresal  46803  dfnbgr5  47837  dfnbgr6  47843  isubgruhgr  47854  stgrnbgr0  47931  lines  48652  rrxlines  48654  eenglngeehlnm  48660  clddisj  48801  iscnrm3rlem1  48837