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 18	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  difeq12d  4067  dffv2  7006  on2recsov  8708  phplem2  9251  unfilem3  9330  marypha1lem  9455  infdifsn  9688  cantnfp1lem3  9711  en2other2  10118  isacn  10153  fin23lem28  10448  enfin1ai  10492  fin1a2lem7  10514  fzdifsuc  13748  axdc4uz  14157  leiso  14634  cshimadifsn  15011  isstruct2  17359  strle1  17368  setsfun0  17382  pltfval  18535  ischn  18813  chnind  18827  chnccats1  18831  chnccat  18832  f1omvdco2  19695  symgsssg  19714  symgfisg  19715  symggen  19717  pmtrdifellem3  19725  pmtrdifwrdellem3  19730  pmtrdifwrdel2lem1  19731  pmtrdifwrdel  19732  pmtrdifwrdel2  19733  psgnunilem1  19740  psgnunilem5  19741  psgnunilem2  19742  psgnunilem3  19743  gsumval3  20154  dmdprd  20247  dprd2da  20291  dmdprdsplit2lem  20294  dpjfval  20304  ablfac1eulem  20321  subdrgint  21093  lssset  21241  lbspropd  21407  islindf  22151  islindf2  22153  f1lindf  22161  opsrtoslem2  22398  cldval  23374  difopn  23385  mretopd  23443  restcld  23523  ordtcld1  23548  ordtcld2  23549  cnclima  23619  iscncl  23620  isreg2  23728  llycmpkgen2  23902  1stckgen  23906  ptval  23922  txcld  23955  ptcld  23965  txkgen  24004  qtopcld  24065  qtoprest  24069  qtopcmap  24071  kqcldsat  24085  regr1lem  24091  trufil  24262  ufildr  24283  opnsubg  24460  cldsubg  24463  blcld  24857  lebnumlem1  25315  bcthlem1  25678  bcth  25683  bcth3  25685  difmbl  25897  itg1val  26037  itgioo  26169  limciun  26247  dvfval  26250  newval  28254  noxpordpred  28372  istrkgl  28953  ishpg  29270  tgplnfn  29286  plngval  29288  isplng  29289  plng3p  29308  eengv  29590  elntg  29595  isuhgr  29671  isushgr  29672  uhgreq12g  29676  isuhgrop  29681  uhgr0vb  29683  uhgrun  29685  uhgrstrrepe  29689  isupgr  29695  upgrop  29705  isumgr  29706  upgrun  29729  isuspgr  29766  isusgr  29767  isuspgrop  29775  nb3grprlem2  29995  uvtxval  30001  nbupgruvtxres  30021  cplgrop  30051  cusgrexi  30057  structtocusgr  30060  1loopgrnb0  30116  cyclnumvtx  30421  isconngr1  30824  frgr3v  30909  difuncomp  33223  imadifxp  33270  fresunsn  33294  fressupp  33355  supppreima  33358  mptiffisupp  33360  gtiso  33368  difico  33448  fzdif2  33455  fzodif2  33456  fzodif1  33457  nn0diffz0  33459  pmtrcnel2  33727  cycpmconjvlem  33778  cycpmrn  33780  tocyccntz  33781  submarchi  33823  elrgspnlem4  33882  isedom  33934  fracfld  33954  elrspunidl  34062  psrbasfsupp  34226  qtophaus  34551  difelsiga  34850  imambfm  34977  difelcarsg  35025  carsgclctunlem1  35032  carsggect  35033  issibf  35048  sibf0  35049  sitgfval  35056  ballotlemfval  35205  ballotlemfp1  35207  ballotlemgun  35240  hgt750lemb  35368  kur14  36161  iscvm  36204  cvmscld  36218  satf  36298  mdvval  36449  topbnd  37303  pibp21  38543  poimirlem2  38745  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem11  38754  poimirlem12  38755  poimirlem13  38756  poimirlem14  38757  poimirlem16  38759  poimirlem18  38761  poimirlem19  38762  poimirlem21  38764  poimirlem22  38765  poimirlem23  38766  poimirlem27  38770  poimirlem30  38773  mblfinlem3  38782  mblfinlem4  38783  itg2addnclem  38794  itg2addnclem2  38795  prjspeclsp  43844  aomclem8  44267  kelac2  44271  gneispace2  45335  fzdifsuc2  46541  iccdifioo  46742  iccdifprioo  46743  ibliooicc  47196  dirkercncflem2  47329  issal  47539  prsal  47543  saldifcl2  47553  intsal  47555  sge0fodjrnlem  47641  caratheodorylem1  47751  vonvolmbllem  47885  salpreimagelt  47932  salpreimalegt  47934  smfresal  48013  chnsubseq  48105  dfnbgr5  49164  dfnbgr6  49170  isubgruhgr  49181  stgrnbgr0  49277  lines  50059  rrxlines  50061  clddisj  50233  iscnrm3rlem1  50269