Theorem peano2 6718

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 6713	. 2 |- ( A e. om <-> suc A e. om )
2	1	biimpi 198	1 |- ( A e. om -> suc A e. om )

Syntax hints:   -> wi 4   e. wcel 1889   suc csuc 5428   omcom 6697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-tr 4501  df-eprel 4748  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-om 6698

This theorem is referenced by:  onnseq  7068  seqomlem1  7172  seqomlem4  7175  onasuc  7235  onmsuc  7236  onesuc  7237  nnacl  7317  nnecl  7319  nnacom  7323  nnmsucr  7331  1onn  7345  2onn  7346  3onn  7347  4onn  7348  nnneo  7357  nneob  7358  omopthlem1  7361  onomeneq  7767  dif1en  7809  findcard  7815  findcard2  7816  unbnn2  7833  dffi3  7950  wofib  8065  axinf2  8150  dfom3  8157  noinfep  8170  cantnflt  8182  trcl  8217  cardsucnn  8424  dif1card  8446  fseqdom  8462  alephfp  8544  ackbij1lem16  8670  ackbij2lem2  8675  ackbij2lem3  8676  ackbij2  8678  sornom  8712  infpssrlem4  8741  fin23lem26  8760  fin23lem20  8772  fin23lem38  8784  fin23lem39  8785  isf32lem2  8789  isf32lem3  8790  isf34lem7  8814  isf34lem6  8815  fin1a2lem6  8840  fin1a2lem9  8843  fin1a2lem12  8846  domtriomlem  8877  axdc2lem  8883  axdc3lem  8885  axdc3lem2  8886  axdc3lem4  8888  axdc4lem  8890  axdclem2  8955  peano2nn  10628  om2uzrani  12173  uzrdgsuci  12181  fzennn  12188  axdc4uzlem  12202  bnj970  29770  trpredtr  30483  elhf2  30954  0hf  30956  hfsn  30958  hfpw  30964  neibastop2lem  31028  finxpsuclem  31801