Theorem difeq1d 4076

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∖ cdif 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-dif 3905

This theorem is used by:  difeq12d  4078  dffv2  6977  on2recsov  8660  phplem2  9203  unfilem3  9281  marypha1lem  9407  infdifsn  9640  cantnfp1lem3  9663  en2other2  10016  isacn  10051  fin23lem28  10346  enfin1ai  10390  fin1a2lem7  10412  fzdifsuc  13643  axdc4uz  14052  leiso  14528  cshimadifsn  14904  isstruct2  17247  strle1  17256  setsfun0  17270  pltfval  18423  ischn  18701  chnind  18715  chnccats1  18719  chnccat  18720  f1omvdco2  19581  symgsssg  19600  symgfisg  19601  symggen  19603  pmtrdifellem3  19611  pmtrdifwrdellem3  19616  pmtrdifwrdel2lem1  19617  pmtrdifwrdel  19618  pmtrdifwrdel2  19619  psgnunilem1  19626  psgnunilem5  19627  psgnunilem2  19628  psgnunilem3  19629  gsumval3  20040  dmdprd  20133  dprd2da  20177  dmdprdsplit2lem  20180  dpjfval  20190  ablfac1eulem  20207  subdrgint  20975  lssset  21123  lbspropd  21289  islindf  22031  islindf2  22033  f1lindf  22041  opsrtoslem2  22278  cldval  23254  difopn  23265  mretopd  23323  restcld  23403  ordtcld1  23428  ordtcld2  23429  cnclima  23499  iscncl  23500  isreg2  23608  llycmpkgen2  23782  1stckgen  23786  ptval  23802  txcld  23835  ptcld  23845  txkgen  23884  qtopcld  23945  qtoprest  23949  qtopcmap  23951  kqcldsat  23965  regr1lem  23971  trufil  24142  ufildr  24163  opnsubg  24340  cldsubg  24343  blcld  24737  lebnumlem1  25195  bcthlem1  25558  bcth  25563  bcth3  25565  difmbl  25777  itg1val  25917  itgioo  26050  limciun  26128  dvfval  26131  newval  28108  noxpordpred  28226  istrkgl  28807  ishpg  29124  tgplnfn  29140  plngval  29142  isplng  29143  plng3p  29162  eengv  29444  elntg  29449  isuhgr  29525  isushgr  29526  uhgreq12g  29530  isuhgrop  29535  uhgr0vb  29537  uhgrun  29539  uhgrstrrepe  29543  isupgr  29549  upgrop  29559  isumgr  29560  upgrun  29583  isuspgr  29620  isusgr  29621  isuspgrop  29629  nb3grprlem2  29849  uvtxval  29855  nbupgruvtxres  29875  cplgrop  29905  cusgrexi  29911  structtocusgr  29914  1loopgrnb0  29970  cyclnumvtx  30275  isconngr1  30678  frgr3v  30763  difuncomp  33035  imadifxp  33082  fresunsn  33106  fressupp  33168  supppreima  33171  mptiffisupp  33173  gtiso  33181  difico  33262  fzdif2  33269  fzodif2  33270  fzodif1  33271  nn0diffz0  33273  pmtrcnel2  33538  cycpmconjvlem  33589  cycpmrn  33591  tocyccntz  33592  submarchi  33634  elrgspnlem4  33693  fracfld  33757  elrspunidl  33864  psrbasfsupp  34029  qtophaus  34354  difelsiga  34653  imambfm  34781  difelcarsg  34829  carsgclctunlem1  34836  carsggect  34837  issibf  34852  sibf0  34853  sitgfval  34860  ballotlemfval  35009  ballotlemfp1  35011  ballotlemgun  35044  hgt750lemb  35172  kur14  35803  iscvm  35846  cvmscld  35860  satf  35940  mdvval  36091  topbnd  36951  pibp21  38177  poimirlem2  38379  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem14  38391  poimirlem16  38393  poimirlem18  38395  poimirlem19  38396  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem27  38404  poimirlem30  38407  mblfinlem3  38416  mblfinlem4  38417  itg2addnclem  38428  itg2addnclem2  38429  prjspeclsp  43466  aomclem8  43910  kelac2  43914  gneispace2  44980  fzdifsuc2  46151  iccdifioo  46353  iccdifprioo  46354  ibliooicc  46807  dirkercncflem2  46940  issal  47150  prsal  47154  saldifcl2  47164  intsal  47166  sge0fodjrnlem  47252  caratheodorylem1  47362  vonvolmbllem  47496  salpreimagelt  47543  salpreimalegt  47545  smfresal  47624  chnsubseq  47716  dfnbgr5  48775  dfnbgr6  48781  isubgruhgr  48792  stgrnbgr0  48888  lines  49669  rrxlines  49671  eenglngeehlnm  49677  clddisj  49838  iscnrm3rlem1  49874