Theorem sucid 5804

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

Step	Hyp	Ref	Expression
1		sucid.1	. 2 |- A e. _V
2		sucidg 5803	. 2 |- ( A e. _V -> A e. suc A )
3	1, 2	ax-mp 5	1 |- A e. suc A

Syntax hints:   e. wcel 1990   _Vcvv 3200   suc csuc 5725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-suc 5729

This theorem is referenced by:  eqelsuc  5806  unon  7031  onuninsuci  7040  tfinds  7059  peano5  7089  tfrlem16  7489  oawordeulem  7634  oalimcl  7640  omlimcl  7658  oneo  7661  omeulem1  7662  oeworde  7673  nnawordex  7717  nnneo  7731  phplem4  8142  php  8144  fiint  8237  inf0  8518  oancom  8548  cantnfval2  8566  cantnflt  8569  cantnflem1  8586  cnfcom  8597  cnfcom2  8599  cnfcom3lem  8600  cnfcom3  8601  r1val1  8649  rankxplim3  8744  cardlim  8798  fseqenlem1  8847  cardaleph  8912  pwsdompw  9026  cfsmolem  9092  axdc3lem4  9275  ttukeylem5  9335  ttukeylem6  9336  ttukeylem7  9337  canthp1lem2  9475  pwxpndom2  9487  winainflem  9515  winalim2  9518  nqereu  9751  bnj216  30800  bnj98  30937  dfrdg2  31701  dford3lem2  37594  pw2f1ocnv  37604  aomclem1  37624