Theorem difeq1d 4077

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

Syntax hints:   → wi 4   = wceq 1559   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3905

This theorem is referenced by:  difeq12d  4079  dffv2  6956  on2recsov  8631  phplem2  9166  unfilem3  9244  marypha1lem  9372  infdifsn  9605  cantnfp1lem3  9628  en2other2  9958  isacn  9993  fin23lem28  10290  enfin1ai  10334  fin1a2lem7  10356  fzdifsuc  13582  axdc4uz  13990  leiso  14465  cshimadifsn  14835  isstruct2  17175  strle1  17184  setsfun0  17198  pltfval  18351  ischn  18629  chnind  18643  chnccats1  18647  chnccat  18648  f1omvdco2  19478  symgsssg  19497  symgfisg  19498  symggen  19500  pmtrdifellem3  19508  pmtrdifwrdellem3  19513  pmtrdifwrdel2lem1  19514  pmtrdifwrdel  19515  pmtrdifwrdel2  19516  psgnunilem1  19523  psgnunilem5  19524  psgnunilem2  19525  psgnunilem3  19526  gsumval3  19937  dmdprd  20030  dprd2da  20074  dmdprdsplit2lem  20077  dpjfval  20087  ablfac1eulem  20104  subdrgint  20839  lssset  20987  lbspropd  21153  islindf  21851  islindf2  21853  f1lindf  21861  opsrtoslem2  22096  cldval  23070  difopn  23081  mretopd  23139  restcld  23219  ordtcld1  23244  ordtcld2  23245  cnclima  23315  iscncl  23316  isreg2  23424  llycmpkgen2  23597  1stckgen  23601  ptval  23617  txcld  23650  ptcld  23660  txkgen  23699  qtopcld  23760  qtoprest  23764  qtopcmap  23766  kqcldsat  23780  regr1lem  23786  trufil  23957  ufildr  23978  opnsubg  24155  cldsubg  24158  blcld  24552  lebnumlem1  25010  bcthlem1  25373  bcth  25378  bcth3  25380  difmbl  25592  itg1val  25732  itgioo  25865  limciun  25943  dvfval  25946  newval  27915  noxpordpred  28033  istrkgl  28614  ishpg  28915  eengv  29136  elntg  29141  isuhgr  29217  isushgr  29218  uhgreq12g  29222  isuhgrop  29227  uhgr0vb  29229  uhgrun  29231  uhgrstrrepe  29235  isupgr  29241  upgrop  29251  isumgr  29252  upgrun  29275  isuspgr  29309  isusgr  29310  isuspgrop  29318  nb3grprlem2  29538  uvtxval  29544  nbupgruvtxres  29564  cplgrop  29594  cusgrexi  29600  structtocusgr  29603  1loopgrnb0  29659  cyclnumvtx  29956  isconngr1  30348  frgr3v  30433  difuncomp  32712  imadifxp  32760  fresunsn  32787  fressupp  32850  supppreima  32853  mptiffisupp  32855  gtiso  32863  difico  32945  fzdif2  32952  fzodif2  32953  fzodif1  32954  nn0diffz0  32956  pmtrcnel2  33230  cycpmconjvlem  33281  cycpmrn  33283  tocyccntz  33284  submarchi  33326  elrgspnlem4  33386  fracfld  33455  elrspunidl  33574  psrbasfsupp  33768  qtophaus  34093  imambfm  34519  difelcarsg  34567  carsgclctunlem1  34574  carsggect  34575  issibf  34590  sibf0  34591  sitgfval  34598  ballotlemfval  34747  ballotlemfp1  34749  ballotlemgun  34782  hgt750lemb  34910  kur14  35526  iscvm  35569  cvmscld  35583  satf  35663  mdvval  35814  topbnd  36644  pibp21  37869  poimirlem2  38081  poimirlem4  38083  poimirlem6  38085  poimirlem7  38086  poimirlem8  38087  poimirlem11  38090  poimirlem12  38091  poimirlem13  38092  poimirlem14  38093  poimirlem16  38095  poimirlem18  38097  poimirlem19  38098  poimirlem21  38100  poimirlem22  38101  poimirlem23  38102  poimirlem27  38106  poimirlem30  38109  mblfinlem3  38118  mblfinlem4  38119  itg2addnclem  38130  itg2addnclem2  38131  prjspeclsp  43154  aomclem8  43598  kelac2  43602  gneispace2  44668  fzdifsuc2  45849  iccdifioo  46051  iccdifprioo  46052  ibliooicc  46505  dirkercncflem2  46638  issal  46848  prsal  46852  saldifcl2  46862  intsal  46864  sge0fodjrnlem  46950  caratheodorylem1  47060  vonvolmbllem  47194  salpreimagelt  47241  salpreimalegt  47243  smfresal  47322  chnsubseq  47416  dfnbgr5  48433  dfnbgr6  48439  isubgruhgr  48450  stgrnbgr0  48546  lines  49313  rrxlines  49315  eenglngeehlnm  49321  clddisj  49485  iscnrm3rlem1  49521