Theorem difeq1d 3689

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

Syntax hints:   → wi 4   = wceq 1475   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-dif 3543

This theorem is referenced by:  difeq12d  3691  diftpsn3OLD  4274  dffv2  6181  phplem4  8027  unfilem3  8111  marypha1lem  8222  infdifsn  8437  cantnfp1lem3  8460  en2other2  8715  isacn  8750  cda1dif  8881  fin23lem28  9045  enfin1ai  9089  fin1a2lem7  9111  fzdifsuc  12270  axdc4uz  12645  leiso  13100  cshimadifsn  13426  isstruct2  15704  setsfun0  15726  strle1  15800  pltfval  16782  f1omvdco2  17691  symgsssg  17710  symgfisg  17711  symggen  17713  pmtrdifellem3  17721  pmtrdifwrdellem3  17726  pmtrdifwrdel2lem1  17727  pmtrdifwrdel  17728  pmtrdifwrdel2  17729  psgnunilem1  17736  psgnunilem5  17737  psgnunilem2  17738  psgnunilem3  17739  gsumval3  18131  dmdprd  18220  dprd2da  18264  dmdprdsplit2lem  18267  dpjfval  18277  ablfac1eulem  18294  lssset  18755  lbspropd  18920  opsrtoslem2  19306  islindf  19970  islindf2  19972  f1lindf  19980  cldval  20637  difopn  20648  mretopd  20706  restcld  20786  ordtcld1  20811  ordtcld2  20812  cnclima  20882  iscncl  20883  isreg2  20991  llycmpkgen2  21163  1stckgen  21167  ptval  21183  txcld  21216  ptcld  21226  txkgen  21265  qtopcld  21326  qtoprest  21330  qtopcmap  21332  kqcldsat  21346  regr1lem  21352  trufil  21524  ufildr  21545  opnsubg  21721  cldsubg  21724  blcld  22120  lebnumlem1  22568  bcthlem1  22929  bcth  22934  bcth3  22936  difmbl  23118  itg1val  23256  itgioo  23388  limciun  23464  dvfval  23467  istrkgl  25157  ishpg  25451  eengv  25659  elntg  25664  isuhgr  25726  isushgr  25727  uhgreq12g  25731  isuhgrop  25736  uhgr0vb  25738  uhgrun  25740  uhgrstrrepe  25745  isupgr  25751  isumgr  25761  upgrun  25784  isuhgra  25827  isushgra  25830  uhgrac  25834  uhgraeq12d  25836  isumgra  25844  isuslgra  25872  isusgra  25873  usgraeq12d  25891  nb3graprlem2  25981  cusgra3v  25993  isconngra1  26201  frgra3v  26529  difuncomp  28752  imadifxp  28796  gtiso  28861  difico  28935  fzdif2  28939  submarchi  29071  qtophaus  29231  imambfm  29651  difelcarsg  29699  carsgclctunlem1  29706  carsggect  29707  issibf  29722  sibf0  29723  sitgfval  29730  ballotlemfval  29878  ballotlemfp1  29880  ballotlemgun  29913  kur14  30452  iscvm  30495  cvmscld  30509  mdvval  30655  topbnd  31489  poimirlem2  32581  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem16  32595  poimirlem18  32597  poimirlem19  32598  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem27  32606  poimirlem30  32609  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2addnclem2  32632  aomclem8  36649  kelac2  36653  gneispace2  37450  fzdifsuc2  38466  iccdifioo  38588  iccdifprioo  38589  ibliooicc  38863  dirkercncflem2  38997  issal  39210  prsal  39214  saldifcl2  39222  intsal  39224  sge0fodjrnlem  39309  caratheodorylem1  39416  vonvolmbllem  39550  salpreimagelt  39595  salpreimalegt  39597  smfresal  39673  uhgruhgra  40375  uhgrauhgr  40376  isuspgr  40382  isusgr  40383  nb3grprlem2  40609  uvtxaval  40613  nbupgruvtxres  40634  cplgrop  40659  cusgrexi  40662  1loopgrnb0  40717  isconngr1  41357  isfrgr  41430  frgr3v  41445