Theorem nnon 7805

Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)

Assertion

Ref	Expression
nnon	⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Proof of Theorem nnon

Step	Hyp	Ref	Expression
1		omsson 7803	. 2 ⊢ ω ⊆ On
2	1	sseli 3931	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2109  Oncon0 6307  ωcom 7799

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-ss 3920  df-om 7800

This theorem is referenced by:  nnoni  7806  nnord  7807  peano4  7825  findsg  7830  onasuc  8446  onmsuc  8447  nna0  8522  nnm0  8523  nnasuc  8524  nnmsuc  8525  nnesuc  8526  nnecl  8531  nnawordi  8539  nnmword  8551  nnawordex  8555  nnaordex  8556  oaabslem  8565  oaabs  8566  oaabs2  8567  omabslem  8568  omabs  8569  nnneo  8573  nneob  8574  naddoa  8620  omnaddcl  8621  dif1ennn  9076  findcard2  9078  onfin2  9130  nndomo  9131  findcard3  9172  dffi3  9321  card2inf  9447  elom3  9544  cantnfp1lem3  9576  cnfcomlem  9595  cnfcom  9596  cnfcom3  9600  ttrcltr  9612  ttrclselem1  9621  ttrclselem2  9622  finnum  9844  cardnn  9859  nnsdomel  9886  harsucnn  9894  nnadjuALT  10093  ficardun2  10096  ackbij1lem15  10127  ackbij2lem2  10133  ackbij2lem3  10134  ackbij2  10136  fin23lem22  10221  isf32lem5  10251  fin1a2lem4  10297  fin1a2lem9  10302  pwfseqlem3  10554  winainflem  10587  wunr1om  10613  tskr1om  10661  grothomex  10723  pion  10773  om2uzlt2i  13858  madefi  27827  oldfi  27828  precsexlem3  28116  precsexlem4  28117  precsexlem5  28118  om2noseqlt  28198  om2noseqlt2  28199  zs12bday  28361  constrfin  33713  constrextdg2lem  33715  constrext2chnlem  33717  constrfiss  33718  constrllcllem  33719  constrlccllem  33720  constrcccllem  33721  constrcn  33727  constrcjcl  33735  bnj168  34697  satfvsuc  35334  satf0suc  35349  sat1el2xp  35352  fmlasuc0  35357  elhf2  36149  findreccl  36427  rdgeqoa  37344  exrecfnlem  37353  finxpreclem4  37368  finxpreclem6  37370  harinf  43007  onexoegt  43217  oaabsb  43267  nnoeomeqom  43285  cantnfub  43294  dflim5  43302  onmcl  43304  omabs2  43305  tfsconcat0b  43319  naddcnffo  43337  naddonnn  43368  naddwordnexlem0  43369  naddwordnexlem3  43372  oawordex3  43373  naddwordnexlem4  43374  omssrncard  43513  nna1iscard  43518