Theorem peano2 7913

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	⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Proof of Theorem peano2

Step	Hyp	Ref	Expression
1		peano2b 7904	. 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
2	1	biimpi 216	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2106  suc csuc 6388  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-om 7888

This theorem is referenced by:  onnseq  8383  seqomlem1  8489  seqomlem4  8492  onasuc  8565  onmsuc  8566  onesuc  8567  o2p2e4  8578  nnacl  8648  nnecl  8650  nnacom  8654  nnmsucr  8662  nnaordex2  8676  1onnALT  8678  2onnALT  8680  3onn  8681  4onn  8682  nnneo  8692  nneob  8693  omopthlem1  8696  eldifsucnn  8701  findcard  9202  unfi  9210  phplem1  9242  php  9245  onomeneqOLD  9264  dif1ennnALT  9309  unbnn2  9331  dffi3  9469  wofib  9583  axinf2  9678  dfom3  9685  noinfep  9698  cantnflt  9710  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  trcl  9766  cardsucnn  10023  harsucnn  10036  dif1card  10048  fseqdom  10064  alephfp  10146  ackbij1lem5  10261  ackbij1lem16  10272  ackbij2lem2  10277  ackbij2lem3  10278  ackbij2  10280  sornom  10315  infpssrlem4  10344  fin23lem26  10363  fin23lem20  10375  fin23lem38  10387  fin23lem39  10388  isf32lem2  10392  isf32lem3  10393  isf34lem7  10417  isf34lem6  10418  fin1a2lem6  10443  fin1a2lem9  10446  fin1a2lem12  10449  domtriomlem  10480  axdc2lem  10486  axdc3lem  10488  axdc3lem2  10489  axdc3lem4  10491  axdc4lem  10493  axdclem2  10558  peano2nn  12276  om2uzrani  13990  uzrdgsuci  13998  fzennn  14006  axdc4uzlem  14021  precsexlem4  28249  precsexlem5  28250  precsexlem11  28256  noseqp1  28312  om2noseqlt  28320  noseqrdgsuc  28329  n0sbday  28369  dfnns2  28377  pw2bday  28433  zs12bday  28439  bnj970  34940  satfvsuc  35346  satfvsucsuc  35350  gonarlem  35379  goalrlem  35381  satffunlem2lem2  35391  satffunlem2  35393  ex-sategoelelomsuc  35411  elhf2  36157  0hf  36159  hfsn  36161  hfpw  36167  neibastop2lem  36343  exrecfnlem  37362  finxpsuclem  37380  domalom  37387  onexoegt  43233  nnoeomeqom  43302  nna1iscard  43535