Theorem peano2 6703

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 6698	. 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 1842   suc csuc 5411   omcom 6682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-tr 4489  df-eprel 4733  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-om 6683

This theorem is referenced by:  onnseq  7047  seqomlem1  7151  seqomlem4  7154  onasuc  7214  onmsuc  7215  onesuc  7216  nnacl  7296  nnecl  7298  nnacom  7302  nnmsucr  7310  1onn  7324  2onn  7325  3onn  7326  4onn  7327  nnneo  7336  nneob  7337  omopthlem1  7340  onomeneq  7744  dif1en  7786  findcard  7792  findcard2  7793  unbnn2  7810  dffi3  7924  wofib  8003  axinf2  8089  dfom3  8096  noinfep  8108  cantnflt  8122  cantnfltOLD  8152  trcl  8190  cardsucnn  8397  dif1card  8419  fseqdom  8438  alephfp  8520  ackbij1lem16  8646  ackbij2lem2  8651  ackbij2lem3  8652  ackbij2  8654  sornom  8688  infpssrlem4  8717  fin23lem26  8736  fin23lem20  8748  fin23lem38  8760  fin23lem39  8761  isf32lem2  8765  isf32lem3  8766  isf34lem7  8790  isf34lem6  8791  fin1a2lem6  8816  fin1a2lem9  8819  fin1a2lem12  8822  domtriomlem  8853  axdc2lem  8859  axdc3lem  8861  axdc3lem2  8862  axdc3lem4  8864  axdc4lem  8866  axdclem2  8931  peano2nn  10587  om2uzrani  12102  uzrdgsuci  12110  fzennn  12117  axdc4uzlem  12131  bnj970  29319  trpredtr  30031  elhf2  30500  0hf  30502  hfsn  30504  hfpw  30510  neibastop2lem  30575