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

Theorem sucid 4957
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  |-  A  e. 
_V
Assertion
Ref Expression
sucid  |-  A  e. 
suc  A

Proof of Theorem sucid
StepHypRef Expression
1 sucid.1 . 2  |-  A  e. 
_V
2 sucidg 4956 . 2  |-  ( A  e.  _V  ->  A  e.  suc  A )
31, 2ax-mp 5 1  |-  A  e. 
suc  A
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113   suc csuc 4880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-suc 4884
This theorem is referenced by:  eqelsuc  4959  unon  6650  onuninsuci  6659  tfinds  6678  peano5  6707  tfrlem16  7062  oawordeulem  7203  oalimcl  7209  omlimcl  7227  oneo  7230  omeulem1  7231  oeworde  7242  nnawordex  7286  nnneo  7300  phplem4  7699  php  7701  fiint  7797  inf0  8038  oancom  8068  cantnfval2  8088  cantnflt  8091  cantnflem1  8108  cantnfval2OLD  8118  cantnfltOLD  8121  cantnflem1OLD  8131  cnfcom  8144  cnfcom2  8146  cnfcom3lem  8147  cnfcom3  8148  cnfcomOLD  8152  cnfcom2OLD  8154  cnfcom3lemOLD  8155  cnfcom3OLD  8156  r1val1  8204  rankxplim3  8299  cardlim  8353  fseqenlem1  8405  cardaleph  8470  pwsdompw  8584  cfsmolem  8650  axdc3lem4  8833  ttukeylem5  8893  ttukeylem6  8894  ttukeylem7  8895  canthp1lem2  9031  pwxpndom2  9043  winainflem  9071  winalim2  9074  nqereu  9307  dfrdg2  28833  nofulllem5  29071  dford3lem2  30601  pw2f1ocnv  30611  aomclem1  30632  bnj216  32885  bnj98  33022
  Copyright terms: Public domain W3C validator