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

Theorem sucid 4966
 Description: A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
Hypothesis
Ref Expression
sucid.1
Assertion
Ref Expression
sucid

Proof of Theorem sucid
StepHypRef Expression
1 sucid.1 . 2
2 sucidg 4965 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wcel 1819  cvv 3109   csuc 4889 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-sn 4033  df-suc 4893 This theorem is referenced by:  eqelsuc  4968  unon  6665  onuninsuci  6674  tfinds  6693  peano5  6722  tfrlem16  7080  oawordeulem  7221  oalimcl  7227  omlimcl  7245  oneo  7248  omeulem1  7249  oeworde  7260  nnawordex  7304  nnneo  7318  phplem4  7718  php  7720  fiint  7815  inf0  8055  oancom  8085  cantnfval2  8105  cantnflt  8108  cantnflem1  8125  cantnfval2OLD  8135  cantnfltOLD  8138  cantnflem1OLD  8148  cnfcom  8161  cnfcom2  8163  cnfcom3lem  8164  cnfcom3  8165  cnfcomOLD  8169  cnfcom2OLD  8171  cnfcom3lemOLD  8172  cnfcom3OLD  8173  r1val1  8221  rankxplim3  8316  cardlim  8370  fseqenlem1  8422  cardaleph  8487  pwsdompw  8601  cfsmolem  8667  axdc3lem4  8850  ttukeylem5  8910  ttukeylem6  8911  ttukeylem7  8912  canthp1lem2  9048  pwxpndom2  9060  winainflem  9088  winalim2  9091  nqereu  9324  dfrdg2  29402  nofulllem5  29640  dford3lem2  31131  pw2f1ocnv  31141  aomclem1  31162  bnj216  33888  bnj98  34026
 Copyright terms: Public domain W3C validator