Theorem difeq1d 4073

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12d  4075  dffv2  6972  on2recsov  8661  phplem2  9204  unfilem3  9283  marypha1lem  9409  infdifsn  9642  cantnfp1lem3  9665  en2other2  10069  isacn  10104  fin23lem28  10399  enfin1ai  10443  fin1a2lem7  10465  fzdifsuc  13698  axdc4uz  14107  leiso  14584  cshimadifsn  14960  isstruct2  17307  strle1  17316  setsfun0  17330  pltfval  18483  ischn  18761  chnind  18775  chnccats1  18779  chnccat  18780  f1omvdco2  19642  symgsssg  19661  symgfisg  19662  symggen  19664  pmtrdifellem3  19672  pmtrdifwrdellem3  19677  pmtrdifwrdel2lem1  19678  pmtrdifwrdel  19679  pmtrdifwrdel2  19680  psgnunilem1  19687  psgnunilem5  19688  psgnunilem2  19689  psgnunilem3  19690  gsumval3  20101  dmdprd  20194  dprd2da  20238  dmdprdsplit2lem  20241  dpjfval  20251  ablfac1eulem  20268  subdrgint  21040  lssset  21188  lbspropd  21354  islindf  22098  islindf2  22100  f1lindf  22108  opsrtoslem2  22345  cldval  23321  difopn  23332  mretopd  23390  restcld  23470  ordtcld1  23495  ordtcld2  23496  cnclima  23566  iscncl  23567  isreg2  23675  llycmpkgen2  23849  1stckgen  23853  ptval  23869  txcld  23902  ptcld  23912  txkgen  23951  qtopcld  24012  qtoprest  24016  qtopcmap  24018  kqcldsat  24032  regr1lem  24038  trufil  24209  ufildr  24230  opnsubg  24407  cldsubg  24410  blcld  24804  lebnumlem1  25262  bcthlem1  25625  bcth  25630  bcth3  25632  difmbl  25844  itg1val  25984  itgioo  26116  limciun  26194  dvfval  26197  newval  28203  noxpordpred  28321  istrkgl  28902  ishpg  29219  tgplnfn  29235  plngval  29237  isplng  29238  plng3p  29257  eengv  29539  elntg  29544  isuhgr  29620  isushgr  29621  uhgreq12g  29625  isuhgrop  29630  uhgr0vb  29632  uhgrun  29634  uhgrstrrepe  29638  isupgr  29644  upgrop  29654  isumgr  29655  upgrun  29678  isuspgr  29715  isusgr  29716  isuspgrop  29724  nb3grprlem2  29944  uvtxval  29950  nbupgruvtxres  29970  cplgrop  30000  cusgrexi  30006  structtocusgr  30009  1loopgrnb0  30065  cyclnumvtx  30370  isconngr1  30773  frgr3v  30858  difuncomp  33130  imadifxp  33177  fresunsn  33201  fressupp  33263  supppreima  33266  mptiffisupp  33268  gtiso  33276  difico  33357  fzdif2  33364  fzodif2  33365  fzodif1  33366  nn0diffz0  33368  pmtrcnel2  33633  cycpmconjvlem  33684  cycpmrn  33686  tocyccntz  33687  submarchi  33729  elrgspnlem4  33788  fracfld  33852  elrspunidl  33960  psrbasfsupp  34125  qtophaus  34450  difelsiga  34749  imambfm  34877  difelcarsg  34925  carsgclctunlem1  34932  carsggect  34933  issibf  34948  sibf0  34949  sitgfval  34956  ballotlemfval  35105  ballotlemfp1  35107  ballotlemgun  35140  hgt750lemb  35268  kur14  35950  iscvm  35993  cvmscld  36007  satf  36087  mdvval  36238  topbnd  37082  pibp21  38306  poimirlem2  38508  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem11  38517  poimirlem12  38518  poimirlem13  38519  poimirlem14  38520  poimirlem16  38522  poimirlem18  38524  poimirlem19  38525  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem27  38533  poimirlem30  38536  mblfinlem3  38545  mblfinlem4  38546  itg2addnclem  38557  itg2addnclem2  38558  prjspeclsp  43602  aomclem8  44021  kelac2  44025  gneispace2  45091  fzdifsuc2  46269  iccdifioo  46471  iccdifprioo  46472  ibliooicc  46925  dirkercncflem2  47058  issal  47268  prsal  47272  saldifcl2  47282  intsal  47284  sge0fodjrnlem  47370  caratheodorylem1  47480  vonvolmbllem  47614  salpreimagelt  47661  salpreimalegt  47663  smfresal  47742  chnsubseq  47834  dfnbgr5  48893  dfnbgr6  48899  isubgruhgr  48910  stgrnbgr0  49006  lines  49787  rrxlines  49789  eenglngeehlnm  49795  clddisj  49956  iscnrm3rlem1  49992