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

Theorem sucid 5521
 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 5520 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wcel 1870  cvv 3087   csuc 5444 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-sn 4003  df-suc 5448 This theorem is referenced by:  eqelsuc  5523  unon  6672  onuninsuci  6681  tfinds  6700  peano5  6730  tfrlem16  7119  oawordeulem  7263  oalimcl  7269  omlimcl  7287  oneo  7290  omeulem1  7291  oeworde  7302  nnawordex  7346  nnneo  7360  phplem4  7760  php  7762  fiint  7854  inf0  8126  oancom  8156  cantnfval2  8173  cantnflt  8176  cantnflem1  8193  cnfcom  8204  cnfcom2  8206  cnfcom3lem  8207  cnfcom3  8208  r1val1  8256  rankxplim3  8351  cardlim  8405  fseqenlem1  8453  cardaleph  8518  pwsdompw  8632  cfsmolem  8698  axdc3lem4  8881  ttukeylem5  8941  ttukeylem6  8942  ttukeylem7  8943  canthp1lem2  9077  pwxpndom2  9089  winainflem  9117  winalim2  9120  nqereu  9353  bnj216  29328  bnj98  29466  dfrdg2  30229  nofulllem5  30380  dford3lem2  35588  pw2f1ocnv  35598  aomclem1  35618
 Copyright terms: Public domain W3C validator