Theorem difeq1d 4057

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-dif 3891

This theorem is referenced by:  difeq12d  4059  dffv2  6872  phplem2  9000  phplem4OLD  9012  unfilem3  9089  marypha1lem  9201  infdifsn  9424  cantnfp1lem3  9447  en2other2  9774  isacn  9809  fin23lem28  10105  enfin1ai  10149  fin1a2lem7  10171  fzdifsuc  13325  axdc4uz  13713  leiso  14182  cshimadifsn  14551  isstruct2  16859  strle1  16868  setsfun0  16882  pltfval  18058  f1omvdco2  19065  symgsssg  19084  symgfisg  19085  symggen  19087  pmtrdifellem3  19095  pmtrdifwrdellem3  19100  pmtrdifwrdel2lem1  19101  pmtrdifwrdel  19102  pmtrdifwrdel2  19103  psgnunilem1  19110  psgnunilem5  19111  psgnunilem2  19112  psgnunilem3  19113  gsumval3  19517  dmdprd  19610  dprd2da  19654  dmdprdsplit2lem  19657  dpjfval  19667  ablfac1eulem  19684  subdrgint  20080  lssset  20204  lbspropd  20370  islindf  21028  islindf2  21030  f1lindf  21038  opsrtoslem2  21272  cldval  22183  difopn  22194  mretopd  22252  restcld  22332  ordtcld1  22357  ordtcld2  22358  cnclima  22428  iscncl  22429  isreg2  22537  llycmpkgen2  22710  1stckgen  22714  ptval  22730  txcld  22763  ptcld  22773  txkgen  22812  qtopcld  22873  qtoprest  22877  qtopcmap  22879  kqcldsat  22893  regr1lem  22899  trufil  23070  ufildr  23091  opnsubg  23268  cldsubg  23271  blcld  23670  lebnumlem1  24133  bcthlem1  24497  bcth  24502  bcth3  24504  difmbl  24716  itg1val  24856  itgioo  24989  limciun  25067  dvfval  25070  istrkgl  26828  ishpg  27129  eengv  27356  elntg  27361  isuhgr  27439  isushgr  27440  uhgreq12g  27444  isuhgrop  27449  uhgr0vb  27451  uhgrun  27453  uhgrstrrepe  27457  isupgr  27463  upgrop  27473  isumgr  27474  upgrun  27497  isuspgr  27531  isusgr  27532  isuspgrop  27540  nb3grprlem2  27757  uvtxval  27763  nbupgruvtxres  27783  cplgrop  27813  cusgrexi  27819  structtocusgr  27822  1loopgrnb0  27878  isconngr1  28563  frgr3v  28648  difuncomp  30902  imadifxp  30949  fressupp  31031  supppreima  31034  gtiso  31042  difico  31113  fzdif2  31121  fzodif2  31122  fzodif1  31123  pmtrcnel2  31368  cycpmconjvlem  31417  cycpmrn  31419  tocyccntz  31420  submarchi  31449  elrspunidl  31615  qtophaus  31795  imambfm  32238  difelcarsg  32286  carsgclctunlem1  32293  carsggect  32294  issibf  32309  sibf0  32310  sitgfval  32317  ballotlemfval  32465  ballotlemfp1  32467  ballotlemgun  32500  hgt750lemb  32645  kur14  33187  iscvm  33230  cvmscld  33244  satf  33324  mdvval  33475  on2recsov  33836  newval  34048  noxpordpred  34119  topbnd  34522  pibp21  35595  poimirlem2  35788  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem16  35802  poimirlem18  35804  poimirlem19  35805  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem27  35813  poimirlem30  35816  mblfinlem3  35825  mblfinlem4  35826  itg2addnclem  35837  itg2addnclem2  35838  prjspeclsp  40458  aomclem8  40893  kelac2  40897  gneispace2  41749  fzdifsuc2  42856  iccdifioo  43060  iccdifprioo  43061  ibliooicc  43519  dirkercncflem2  43652  issal  43862  prsal  43866  saldifcl2  43874  intsal  43876  sge0fodjrnlem  43961  caratheodorylem1  44071  vonvolmbllem  44205  salpreimagelt  44252  salpreimalegt  44254  smfresal  44333  lines  46088  rrxlines  46090  eenglngeehlnm  46096  clddisj  46208  iscnrm3rlem1  46245