Theorem peano2 6704

Description: The successor of any natural number is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
peano2	|- ( A e. om -> suc A e. om )

Proof of Theorem peano2

Step	Hyp	Ref	Expression
1		peano2b 6700	. 2 |- ( A e. om <-> suc A e. om )
2	1	biimpi 194	1 |- ( A e. om -> suc A e. om )

Syntax hints:   -> wi 4   e. wcel 1767   suc csuc 4880   omcom 6684

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-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-tr 4541  df-eprel 4791  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-om 6685

This theorem is referenced by:  onnseq  7015  seqomlem1  7115  seqomlem4  7118  onasuc  7178  onmsuc  7179  onesuc  7180  nnacl  7260  nnecl  7262  nnacom  7266  nnmsucr  7274  1onn  7288  2onn  7289  3onn  7290  4onn  7291  nnneo  7300  nneob  7301  omopthlem1  7304  onomeneq  7707  dif1enOLD  7752  dif1en  7753  findcard  7759  findcard2  7760  unbnn2  7777  dffi3  7891  wofib  7970  axinf2  8057  dfom3  8064  noinfep  8076  noinfepOLD  8077  cantnflt  8091  cantnfltOLD  8121  trcl  8159  cardsucnn  8366  dif1card  8388  fseqdom  8407  alephfp  8489  ackbij1lem16  8615  ackbij2lem2  8620  ackbij2lem3  8621  ackbij2  8623  sornom  8657  infpssrlem4  8686  fin23lem26  8705  fin23lem20  8717  fin23lem38  8729  fin23lem39  8730  isf32lem2  8734  isf32lem3  8735  isf34lem7  8759  isf34lem6  8760  fin1a2lem6  8785  fin1a2lem9  8788  fin1a2lem12  8791  domtriomlem  8822  axdc2lem  8828  axdc3lem  8830  axdc3lem2  8831  axdc3lem4  8833  axdc4lem  8835  axdclem2  8900  peano2nn  10548  om2uzrani  12031  uzrdgsuci  12039  fzennn  12046  axdc4uzlem  12060  trpredtr  28918  elhf2  29437  0hf  29439  hfsn  29441  hfpw  29447  neibastop2lem  29809  bnj970  33102