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

Theorem sucid 4787
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 4786 . 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 1757   _Vcvv 2964   suc csuc 4710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2966  df-un 3323  df-sn 3868  df-suc 4714
This theorem is referenced by:  eqelsuc  4789  unon  6433  onuninsuci  6442  tfinds  6461  peano5  6490  tfrlem16  6840  oawordeulem  6983  oalimcl  6989  omlimcl  7007  oneo  7010  omeulem1  7011  oeworde  7022  nnawordex  7066  nnneo  7080  phplem4  7483  php  7485  fiint  7578  inf0  7817  oancom  7847  cantnfval2  7867  cantnflt  7870  cantnflem1  7887  cantnfval2OLD  7897  cantnfltOLD  7900  cantnflem1OLD  7910  cnfcom  7923  cnfcom2  7925  cnfcom3lem  7926  cnfcom3  7927  cnfcomOLD  7931  cnfcom2OLD  7933  cnfcom3lemOLD  7934  cnfcom3OLD  7935  r1val1  7983  rankxplim3  8078  cardlim  8132  fseqenlem1  8184  cardaleph  8249  pwsdompw  8363  cfsmolem  8429  axdc3lem4  8612  ttukeylem5  8672  ttukeylem6  8673  ttukeylem7  8674  canthp1lem2  8810  pwxpndom2  8822  winainflem  8850  winalim2  8853  nqereu  9088  dfrdg2  27458  nofulllem5  27696  dford3lem2  29223  pw2f1ocnv  29233  aomclem1  29254  bnj216  31465  bnj98  31602
  Copyright terms: Public domain W3C validator