Theorem difeq1d 4079

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  difeq12d  4081  dffv2  6937  on2recsov  8606  phplem2  9141  unfilem3  9219  marypha1lem  9348  infdifsn  9578  cantnfp1lem3  9601  en2other2  9931  isacn  9966  fin23lem28  10262  enfin1ai  10306  fin1a2lem7  10328  fzdifsuc  13512  axdc4uz  13919  leiso  14394  cshimadifsn  14764  isstruct2  17088  strle1  17097  setsfun0  17111  pltfval  18264  ischn  18542  chnind  18556  chnccats1  18560  chnccat  18561  f1omvdco2  19389  symgsssg  19408  symgfisg  19409  symggen  19411  pmtrdifellem3  19419  pmtrdifwrdellem3  19424  pmtrdifwrdel2lem1  19425  pmtrdifwrdel  19426  pmtrdifwrdel2  19427  psgnunilem1  19434  psgnunilem5  19435  psgnunilem2  19436  psgnunilem3  19437  gsumval3  19848  dmdprd  19941  dprd2da  19985  dmdprdsplit2lem  19988  dpjfval  19998  ablfac1eulem  20015  subdrgint  20748  lssset  20896  lbspropd  21063  islindf  21779  islindf2  21781  f1lindf  21789  opsrtoslem2  22023  cldval  22979  difopn  22990  mretopd  23048  restcld  23128  ordtcld1  23153  ordtcld2  23154  cnclima  23224  iscncl  23225  isreg2  23333  llycmpkgen2  23506  1stckgen  23510  ptval  23526  txcld  23559  ptcld  23569  txkgen  23608  qtopcld  23669  qtoprest  23673  qtopcmap  23675  kqcldsat  23689  regr1lem  23695  trufil  23866  ufildr  23887  opnsubg  24064  cldsubg  24067  blcld  24461  lebnumlem1  24928  bcthlem1  25292  bcth  25297  bcth3  25299  difmbl  25512  itg1val  25652  itgioo  25785  limciun  25863  dvfval  25866  newval  27843  noxpordpred  27961  istrkgl  28542  ishpg  28843  eengv  29064  elntg  29069  isuhgr  29145  isushgr  29146  uhgreq12g  29150  isuhgrop  29155  uhgr0vb  29157  uhgrun  29159  uhgrstrrepe  29163  isupgr  29169  upgrop  29179  isumgr  29180  upgrun  29203  isuspgr  29237  isusgr  29238  isuspgrop  29246  nb3grprlem2  29466  uvtxval  29472  nbupgruvtxres  29492  cplgrop  29522  cusgrexi  29528  structtocusgr  29531  1loopgrnb0  29588  cyclnumvtx  29885  isconngr1  30277  frgr3v  30362  difuncomp  32639  imadifxp  32687  fresunsn  32714  fressupp  32777  supppreima  32780  mptiffisupp  32782  gtiso  32790  difico  32873  fzdif2  32880  fzodif2  32881  fzodif1  32882  nn0diffz0  32884  pmtrcnel2  33183  cycpmconjvlem  33234  cycpmrn  33236  tocyccntz  33237  submarchi  33279  elrgspnlem4  33338  fracfld  33401  elrspunidl  33520  psrbasfsupp  33704  qtophaus  34013  imambfm  34439  difelcarsg  34487  carsgclctunlem1  34494  carsggect  34495  issibf  34510  sibf0  34511  sitgfval  34518  ballotlemfval  34667  ballotlemfp1  34669  ballotlemgun  34702  hgt750lemb  34833  kur14  35429  iscvm  35472  cvmscld  35486  satf  35566  mdvval  35717  topbnd  36537  pibp21  37667  poimirlem2  37870  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem11  37879  poimirlem12  37880  poimirlem13  37881  poimirlem14  37882  poimirlem16  37884  poimirlem18  37886  poimirlem19  37887  poimirlem21  37889  poimirlem22  37890  poimirlem23  37891  poimirlem27  37895  poimirlem30  37898  mblfinlem3  37907  mblfinlem4  37908  itg2addnclem  37919  itg2addnclem2  37920  prjspeclsp  42967  aomclem8  43415  kelac2  43419  gneispace2  44485  fzdifsuc2  45669  iccdifioo  45872  iccdifprioo  45873  ibliooicc  46326  dirkercncflem2  46459  issal  46669  prsal  46673  saldifcl2  46683  intsal  46685  sge0fodjrnlem  46771  caratheodorylem1  46881  vonvolmbllem  47015  salpreimagelt  47062  salpreimalegt  47064  smfresal  47143  chnsubseq  47235  dfnbgr5  48208  dfnbgr6  48214  isubgruhgr  48225  stgrnbgr0  48321  lines  49088  rrxlines  49090  eenglngeehlnm  49096  clddisj  49260  iscnrm3rlem1  49296