MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq1d Unicode version

Theorem difeq1d 3620
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
StepHypRef Expression
1 difeq1d.1 . 2
2 difeq1 3614 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  \cdif 3472
This theorem is referenced by:  difeq12d  3622  diftpsn3  4168  dffv2  5946  phplem4  7719  unfilem3  7806  marypha1lem  7913  infdifsn  8094  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  en2other2  8408  isacn  8446  cda1dif  8577  fin23lem28  8741  enfin1ai  8785  fin1a2lem7  8807  fzdifsuc  11768  axdc4uz  12093  leiso  12508  isstruct2  14641  strle1  14728  pltfval  15589  f1omvdco2  16473  symgsssg  16492  symgfisg  16493  symggen  16495  pmtrdifellem3  16503  pmtrdifwrdellem3  16508  pmtrdifwrdel2lem1  16509  pmtrdifwrdel  16510  pmtrdifwrdel2  16511  psgnunilem1  16518  psgnunilem5  16519  psgnunilem2  16520  psgnunilem3  16521  gsumval3OLD  16908  gsumval3  16911  dmdprd  17029  dprd2da  17091  dmdprdsplit2lem  17094  dpjfval  17104  ablfac1eulem  17123  lssset  17580  lbspropd  17745  opsrtoslem2  18149  islindf  18847  islindf2  18849  f1lindf  18857  cldval  19524  difopn  19535  mretopd  19593  restcld  19673  ordtcld1  19698  ordtcld2  19699  cnclima  19769  iscncl  19770  isreg2  19878  llycmpkgen2  20051  1stckgen  20055  ptval  20071  txcld  20104  ptcld  20114  txkgen  20153  qtopcld  20214  qtoprest  20218  qtopcmap  20220  kqcldsat  20234  regr1lem  20240  trufil  20411  ufildr  20432  opnsubg  20606  cldsubg  20609  blcld  21008  lebnumlem1  21461  bcthlem1  21763  bcth  21768  bcth3  21770  difmbl  21953  itg1val  22090  itgioo  22222  limciun  22298  dvfval  22301  istrkgl  23855  ishpg  24128  eengv  24282  elntg  24287  isuhgra  24298  isushgra  24301  uhgrac  24305  uhgraeq12d  24307  isumgra  24315  isuslgra  24343  isusgra  24344  usgraeq12d  24362  nb3graprlem2  24452  cusgra3v  24464  isconngra1  24673  frgra3v  25002  imadifxp  27458  gtiso  27519  difico  27594  submarchi  27730  qtophaus  27839  imambfm  28233  issibf  28275  sibf0  28276  sitgfval  28283  ballotlemfval  28428  ballotlemfp1  28430  ballotlemgun  28463  kur14  28660  iscvm  28704  cvmscld  28718  mdvval  28864  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem  30066  itg2addnclem2  30067  topbnd  30142  aomclem8  31007  kelac2  31011  fzdifsuc2  31512  iccdifioo  31555  iccdifprioo  31556  ibliooicc  31770  dirkercncflem2  31886  isuhgr  32366  isushgr  32367  uhgeq12g  32370  uhguhgra  32372  uhgrauhg  32373  uhg0v  32377  uhgun  32380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-dif 3478
  Copyright terms: Public domain W3C validator