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

Theorem suceq 4948
Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
suceq

Proof of Theorem suceq
StepHypRef Expression
1 id 22 . . 3
2 sneq 4039 . . 3
31, 2uneq12d 3658 . 2
4 df-suc 4889 . 2
5 df-suc 4889 . 2
63, 4, 53eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  u.cun 3473  {csn 4029  succsuc 4885
This theorem is referenced by:  eqelsuc  4964  suc11  4986  ordunisuc  6667  onsucuni2  6669  onuninsuci  6675  limsuc  6684  tfindes  6697  tfinds2  6698  findes  6730  onnseq  7034  seqomlem0  7133  seqomlem1  7134  seqomlem4  7137  oasuc  7193  onasuc  7197  oa1suc  7200  oa0r  7207  oaass  7229  oneo  7249  omeulem1  7250  oeeulem  7269  oeeui  7270  nna0r  7277  nnacom  7285  nnaass  7290  nnmsucr  7293  omabs  7315  nnneo  7319  nneob  7320  omsmolem  7321  omopthlem1  7323  limensuc  7714  infensuc  7715  nneneq  7720  unblem2  7793  unblem3  7794  suc11reg  8057  inf0  8059  inf3lem1  8066  dfom3  8085  cantnflt  8112  cantnflem1  8129  cantnfltOLD  8142  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  r1elwf  8235  rankidb  8239  rankonidlem  8267  ranklim  8283  rankopb  8291  rankelop  8313  rankxpu  8315  rankmapu  8317  rankxplim  8318  cardsucnn  8387  dif1card  8409  infxpenlem  8412  fseqenlem1  8426  dfac12lem1  8544  dfac12lem2  8545  dfac12r  8547  pwsdompw  8605  ackbij1lem5  8625  ackbij1lem14  8634  ackbij1lem18  8638  ackbij1  8639  ackbij2lem3  8642  cfsmolem  8671  cfsmo  8672  sornom  8678  isfin3ds  8730  isf32lem1  8754  isf32lem2  8755  isf32lem5  8758  isf32lem6  8759  isf32lem7  8760  isf32lem8  8761  isf32lem11  8764  fin1a2lem1  8801  ituniiun  8823  axdc2lem  8849  axdc3lem2  8852  axdc3lem3  8853  axdc3lem4  8854  axdc3  8855  axdc4lem  8856  axcclem  8858  axdclem2  8921  wunex2  9137  om2uzsuci  12059  axdc4uzlem  12092  nofulllem1  29462  nofulllem2  29463  rankaltopb  29629  ranksng  29824  rankpwg  29826  rankeq1o  29828  ontgsucval  29897  onsuccon  29903  onsucsuccmp  29909  limsucncmp  29911  ordcmp  29912  limsuc2  30986  aomclem4  31003  aomclem8  31007  bnj222  33941  bnj966  34002  bnj1112  34039
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-or 370  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-v 3111  df-un 3480  df-sn 4030  df-suc 4889
  Copyright terms: Public domain W3C validator