Theorem difeq1d 4088

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-dif 3917

This theorem is referenced by:  difeq12d  4090  dffv2  6956  on2recsov  8632  phplem2  9169  unfilem3  9256  marypha1lem  9384  infdifsn  9610  cantnfp1lem3  9633  en2other2  9962  isacn  9997  fin23lem28  10293  enfin1ai  10337  fin1a2lem7  10359  fzdifsuc  13545  axdc4uz  13949  leiso  14424  cshimadifsn  14795  isstruct2  17119  strle1  17128  setsfun0  17142  pltfval  18290  f1omvdco2  19378  symgsssg  19397  symgfisg  19398  symggen  19400  pmtrdifellem3  19408  pmtrdifwrdellem3  19413  pmtrdifwrdel2lem1  19414  pmtrdifwrdel  19415  pmtrdifwrdel2  19416  psgnunilem1  19423  psgnunilem5  19424  psgnunilem2  19425  psgnunilem3  19426  gsumval3  19837  dmdprd  19930  dprd2da  19974  dmdprdsplit2lem  19977  dpjfval  19987  ablfac1eulem  20004  subdrgint  20712  lssset  20839  lbspropd  21006  islindf  21721  islindf2  21723  f1lindf  21731  opsrtoslem2  21963  cldval  22910  difopn  22921  mretopd  22979  restcld  23059  ordtcld1  23084  ordtcld2  23085  cnclima  23155  iscncl  23156  isreg2  23264  llycmpkgen2  23437  1stckgen  23441  ptval  23457  txcld  23490  ptcld  23500  txkgen  23539  qtopcld  23600  qtoprest  23604  qtopcmap  23606  kqcldsat  23620  regr1lem  23626  trufil  23797  ufildr  23818  opnsubg  23995  cldsubg  23998  blcld  24393  lebnumlem1  24860  bcthlem1  25224  bcth  25229  bcth3  25231  difmbl  25444  itg1val  25584  itgioo  25717  limciun  25795  dvfval  25798  newval  27763  noxpordpred  27860  istrkgl  28385  ishpg  28686  eengv  28906  elntg  28911  isuhgr  28987  isushgr  28988  uhgreq12g  28992  isuhgrop  28997  uhgr0vb  28999  uhgrun  29001  uhgrstrrepe  29005  isupgr  29011  upgrop  29021  isumgr  29022  upgrun  29045  isuspgr  29079  isusgr  29080  isuspgrop  29088  nb3grprlem2  29308  uvtxval  29314  nbupgruvtxres  29334  cplgrop  29364  cusgrexi  29370  structtocusgr  29373  1loopgrnb0  29430  cyclnumvtx  29730  isconngr1  30119  frgr3v  30204  difuncomp  32482  imadifxp  32530  fressupp  32611  supppreima  32614  mptiffisupp  32616  gtiso  32624  difico  32706  fzdif2  32713  fzodif2  32714  fzodif1  32715  ischn  32932  chnind  32937  chnccats1  32941  pmtrcnel2  33047  cycpmconjvlem  33098  cycpmrn  33100  tocyccntz  33101  submarchi  33140  elrgspnlem4  33196  fracfld  33258  elrspunidl  33399  qtophaus  33826  imambfm  34253  difelcarsg  34301  carsgclctunlem1  34308  carsggect  34309  issibf  34324  sibf0  34325  sitgfval  34332  ballotlemfval  34481  ballotlemfp1  34483  ballotlemgun  34516  hgt750lemb  34647  kur14  35203  iscvm  35246  cvmscld  35260  satf  35340  mdvval  35491  topbnd  36312  pibp21  37403  poimirlem2  37616  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem18  37632  poimirlem19  37633  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem27  37641  poimirlem30  37644  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  itg2addnclem2  37666  prjspeclsp  42600  aomclem8  43050  kelac2  43054  gneispace2  44121  fzdifsuc2  45308  iccdifioo  45513  iccdifprioo  45514  ibliooicc  45969  dirkercncflem2  46102  issal  46312  prsal  46316  saldifcl2  46326  intsal  46328  sge0fodjrnlem  46414  caratheodorylem1  46524  vonvolmbllem  46658  salpreimagelt  46705  salpreimalegt  46707  smfresal  46786  dfnbgr5  47851  dfnbgr6  47857  isubgruhgr  47868  stgrnbgr0  47963  lines  48720  rrxlines  48722  eenglngeehlnm  48728  clddisj  48892  iscnrm3rlem1  48928