Theorem peano2 7912

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 2108  suc csuc 6386  ωcom 7887

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-om 7888

This theorem is referenced by:  onnseq  8384  seqomlem1  8490  seqomlem4  8493  onasuc  8566  onmsuc  8567  onesuc  8568  o2p2e4  8579  nnacl  8649  nnecl  8651  nnacom  8655  nnmsucr  8663  nnaordex2  8677  1onnALT  8679  2onnALT  8681  3onn  8682  4onn  8683  nnneo  8693  nneob  8694  omopthlem1  8697  eldifsucnn  8702  findcard  9203  unfi  9211  phplem1  9244  php  9247  onomeneqOLD  9266  dif1ennnALT  9311  unbnn2  9333  dffi3  9471  wofib  9585  axinf2  9680  dfom3  9687  noinfep  9700  cantnflt  9712  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  trcl  9768  cardsucnn  10025  harsucnn  10038  dif1card  10050  fseqdom  10066  alephfp  10148  ackbij1lem5  10263  ackbij1lem16  10274  ackbij2lem2  10279  ackbij2lem3  10280  ackbij2  10282  sornom  10317  infpssrlem4  10346  fin23lem26  10365  fin23lem20  10377  fin23lem38  10389  fin23lem39  10390  isf32lem2  10394  isf32lem3  10395  isf34lem7  10419  isf34lem6  10420  fin1a2lem6  10445  fin1a2lem9  10448  fin1a2lem12  10451  domtriomlem  10482  axdc2lem  10488  axdc3lem  10490  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  axdclem2  10560  peano2nn  12278  om2uzrani  13993  uzrdgsuci  14001  fzennn  14009  axdc4uzlem  14024  precsexlem4  28234  precsexlem5  28235  precsexlem11  28241  noseqp1  28297  om2noseqlt  28305  noseqrdgsuc  28314  n0sbday  28354  dfnns2  28362  pw2bday  28418  zs12bday  28424  constrextdg2lem  33789  bnj970  34961  satfvsuc  35366  satfvsucsuc  35370  gonarlem  35399  goalrlem  35401  satffunlem2lem2  35411  satffunlem2  35413  ex-sategoelelomsuc  35431  elhf2  36176  0hf  36178  hfsn  36180  hfpw  36186  neibastop2lem  36361  exrecfnlem  37380  finxpsuclem  37398  domalom  37405  onexoegt  43256  nnoeomeqom  43325  nna1iscard  43558  omssaxinf2  45005