Theorem peano2 7874

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 7865	. 2 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)
2	1	biimpi 215	1 ⊢ (𝐴 ∈ ω → suc 𝐴 ∈ ω)

Syntax hints:   → wi 4   ∈ wcel 2098  suc csuc 6356  ωcom 7848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-tr 5256  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-om 7849

This theorem is referenced by:  onnseq  8339  seqomlem1  8445  seqomlem4  8448  onasuc  8523  onmsuc  8524  onesuc  8525  o2p2e4  8536  nnacl  8606  nnecl  8608  nnacom  8612  nnmsucr  8620  1onnALT  8635  2onnALT  8637  3onn  8638  4onn  8639  nnneo  8649  nneob  8650  omopthlem1  8653  eldifsucnn  8658  findcard  9158  unfi  9167  phplem1  9202  php  9205  onomeneqOLD  9224  dif1ennnALT  9272  findcard2OLD  9279  unbnn2  9295  dffi3  9421  wofib  9535  axinf2  9630  dfom3  9637  noinfep  9650  cantnflt  9662  ttrcltr  9706  ttrclss  9710  ttrclselem2  9716  trcl  9718  cardsucnn  9975  harsucnn  9988  dif1card  10000  fseqdom  10016  alephfp  10098  ackbij1lem5  10214  ackbij1lem16  10225  ackbij2lem2  10230  ackbij2lem3  10231  ackbij2  10233  sornom  10267  infpssrlem4  10296  fin23lem26  10315  fin23lem20  10327  fin23lem38  10339  fin23lem39  10340  isf32lem2  10344  isf32lem3  10345  isf34lem7  10369  isf34lem6  10370  fin1a2lem6  10395  fin1a2lem9  10398  fin1a2lem12  10401  domtriomlem  10432  axdc2lem  10438  axdc3lem  10440  axdc3lem2  10441  axdc3lem4  10443  axdc4lem  10445  axdclem2  10510  peano2nn  12220  om2uzrani  13913  uzrdgsuci  13921  fzennn  13929  axdc4uzlem  13944  precsexlem4  28023  precsexlem5  28024  precsexlem11  28030  peano2n0s  28086  bnj970  34413  satfvsuc  34807  satfvsucsuc  34811  gonarlem  34840  goalrlem  34842  satffunlem2lem2  34852  satffunlem2  34854  ex-sategoelelomsuc  34872  elhf2  35608  0hf  35610  hfsn  35612  hfpw  35618  neibastop2lem  35701  exrecfnlem  36716  finxpsuclem  36734  domalom  36741  onexoegt  42448  nnoeomeqom  42517  nna1iscard  42751