Theorem peano2 7846

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

Syntax hints:   → wi 4   ∈ wcel 2109  suc csuc 6322  ωcom 7822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-om 7823

This theorem is referenced by:  onnseq  8290  seqomlem1  8395  seqomlem4  8398  onasuc  8469  onmsuc  8470  onesuc  8471  o2p2e4  8482  nnacl  8552  nnecl  8554  nnacom  8558  nnmsucr  8566  nnaordex2  8580  1onnALT  8582  2onnALT  8584  3onn  8585  4onn  8586  nnneo  8596  nneob  8597  omopthlem1  8600  eldifsucnn  8605  findcard  9104  unfi  9112  phplem1  9145  php  9148  dif1ennnALT  9198  unbnn2  9220  dffi3  9358  wofib  9474  axinf2  9569  dfom3  9576  noinfep  9589  cantnflt  9601  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  trcl  9657  cardsucnn  9914  harsucnn  9927  dif1card  9939  fseqdom  9955  alephfp  10037  ackbij1lem5  10152  ackbij1lem16  10163  ackbij2lem2  10168  ackbij2lem3  10169  ackbij2  10171  sornom  10206  infpssrlem4  10235  fin23lem26  10254  fin23lem20  10266  fin23lem38  10278  fin23lem39  10279  isf32lem2  10283  isf32lem3  10284  isf34lem7  10308  isf34lem6  10309  fin1a2lem6  10334  fin1a2lem9  10337  fin1a2lem12  10340  domtriomlem  10371  axdc2lem  10377  axdc3lem  10379  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  axdclem2  10449  peano2nn  12174  om2uzrani  13893  uzrdgsuci  13901  fzennn  13909  axdc4uzlem  13924  precsexlem4  28088  precsexlem5  28089  precsexlem11  28095  noseqp1  28161  om2noseqlt  28169  noseqrdgsuc  28178  n0sbday  28220  dfnns2  28237  zs12bday  28319  constrextdg2lem  33711  bnj970  34910  satfvsuc  35321  satfvsucsuc  35325  gonarlem  35354  goalrlem  35356  satffunlem2lem2  35366  satffunlem2  35368  ex-sategoelelomsuc  35386  elhf2  36136  0hf  36138  hfsn  36140  hfpw  36146  neibastop2lem  36321  exrecfnlem  37340  finxpsuclem  37358  domalom  37365  onexoegt  43206  nnoeomeqom  43274  nna1iscard  43507  orbitcl  44920  omssaxinf2  44951