Theorem difeq1d 4062

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4047

This theorem is used by:  difeq12d  4064  dffv2  6980  on2recsov  8680  phplem2  9223  unfilem3  9302  marypha1lem  9428  infdifsn  9661  cantnfp1lem3  9684  en2other2  10091  isacn  10126  fin23lem28  10421  enfin1ai  10465  fin1a2lem7  10487  fzdifsuc  13721  axdc4uz  14130  leiso  14607  cshimadifsn  14984  isstruct2  17332  strle1  17341  setsfun0  17355  pltfval  18508  ischn  18786  chnind  18800  chnccats1  18804  chnccat  18805  f1omvdco2  19667  symgsssg  19686  symgfisg  19687  symggen  19689  pmtrdifellem3  19697  pmtrdifwrdellem3  19702  pmtrdifwrdel2lem1  19703  pmtrdifwrdel  19704  pmtrdifwrdel2  19705  psgnunilem1  19712  psgnunilem5  19713  psgnunilem2  19714  psgnunilem3  19715  gsumval3  20126  dmdprd  20219  dprd2da  20263  dmdprdsplit2lem  20266  dpjfval  20276  ablfac1eulem  20293  subdrgint  21065  lssset  21213  lbspropd  21379  islindf  22123  islindf2  22125  f1lindf  22133  opsrtoslem2  22370  cldval  23346  difopn  23357  mretopd  23415  restcld  23495  ordtcld1  23520  ordtcld2  23521  cnclima  23591  iscncl  23592  isreg2  23700  llycmpkgen2  23874  1stckgen  23878  ptval  23894  txcld  23927  ptcld  23937  txkgen  23976  qtopcld  24037  qtoprest  24041  qtopcmap  24043  kqcldsat  24057  regr1lem  24063  trufil  24234  ufildr  24255  opnsubg  24432  cldsubg  24435  blcld  24829  lebnumlem1  25287  bcthlem1  25650  bcth  25655  bcth3  25657  difmbl  25869  itg1val  26009  itgioo  26141  limciun  26219  dvfval  26222  newval  28226  noxpordpred  28344  istrkgl  28925  ishpg  29242  tgplnfn  29258  plngval  29260  isplng  29261  plng3p  29280  eengv  29562  elntg  29567  isuhgr  29643  isushgr  29644  uhgreq12g  29648  isuhgrop  29653  uhgr0vb  29655  uhgrun  29657  uhgrstrrepe  29661  isupgr  29667  upgrop  29677  isumgr  29678  upgrun  29701  isuspgr  29738  isusgr  29739  isuspgrop  29747  nb3grprlem2  29967  uvtxval  29973  nbupgruvtxres  29993  cplgrop  30023  cusgrexi  30029  structtocusgr  30032  1loopgrnb0  30088  cyclnumvtx  30393  isconngr1  30796  frgr3v  30881  difuncomp  33195  imadifxp  33242  fresunsn  33266  fressupp  33328  supppreima  33331  mptiffisupp  33333  gtiso  33341  difico  33421  fzdif2  33428  fzodif2  33429  fzodif1  33430  nn0diffz0  33432  pmtrcnel2  33697  cycpmconjvlem  33748  cycpmrn  33750  tocyccntz  33751  submarchi  33793  elrgspnlem4  33852  fracfld  33916  elrspunidl  34024  psrbasfsupp  34189  qtophaus  34514  difelsiga  34813  imambfm  34940  difelcarsg  34988  carsgclctunlem1  34995  carsggect  34996  issibf  35011  sibf0  35012  sitgfval  35019  ballotlemfval  35168  ballotlemfp1  35170  ballotlemgun  35203  hgt750lemb  35331  kur14  36067  iscvm  36110  cvmscld  36124  satf  36204  mdvval  36355  topbnd  37204  pibp21  38431  poimirlem2  38633  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem11  38642  poimirlem12  38643  poimirlem13  38644  poimirlem14  38645  poimirlem16  38647  poimirlem18  38649  poimirlem19  38650  poimirlem21  38652  poimirlem22  38653  poimirlem23  38654  poimirlem27  38658  poimirlem30  38661  mblfinlem3  38670  mblfinlem4  38671  itg2addnclem  38682  itg2addnclem2  38683  prjspeclsp  43733  aomclem8  44156  kelac2  44160  gneispace2  45225  fzdifsuc2  46419  iccdifioo  46620  iccdifprioo  46621  ibliooicc  47074  dirkercncflem2  47207  issal  47417  prsal  47421  saldifcl2  47431  intsal  47433  sge0fodjrnlem  47519  caratheodorylem1  47629  vonvolmbllem  47763  salpreimagelt  47810  salpreimalegt  47812  smfresal  47891  chnsubseq  47983  dfnbgr5  49042  dfnbgr6  49048  isubgruhgr  49059  stgrnbgr0  49155  lines  49937  rrxlines  49939  clddisj  50111  iscnrm3rlem1  50147