Theorem nnon 7718

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 7716	. 2 ⊢ ω ⊆ On
2	1	sseli 3917	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2106  Oncon0 6266  ωcom 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-om 7713

This theorem is referenced by:  nnoni  7719  nnord  7720  peano4  7739  findsg  7746  onasuc  8358  onmsuc  8359  nna0  8435  nnm0  8436  nnasuc  8437  nnmsuc  8438  nnesuc  8439  nnecl  8444  nnawordi  8452  nnmword  8464  nnawordex  8468  nnaordex  8469  oaabslem  8477  oaabs  8478  oaabs2  8479  omabslem  8480  omabs  8481  nnneo  8485  nneob  8486  onfin2  9014  nndomo  9016  findcard3  9057  dffi3  9190  card2inf  9314  elom3  9406  cantnfp1lem3  9438  cnfcomlem  9457  cnfcom  9458  cnfcom3  9462  ttrcltr  9474  ttrclselem1  9483  ttrclselem2  9484  finnum  9706  cardnn  9721  nnsdomel  9748  harsucnn  9756  nnadjuALT  9954  ficardun2  9958  ficardun2OLD  9959  ackbij1lem15  9990  ackbij2lem2  9996  ackbij2lem3  9997  ackbij2  9999  fin23lem22  10083  isf32lem5  10113  fin1a2lem4  10159  fin1a2lem9  10164  pwfseqlem3  10416  winainflem  10449  wunr1om  10475  tskr1om  10523  grothomex  10585  pion  10635  om2uzlt2i  13671  bnj168  32709  satfvsuc  33323  satf0suc  33338  sat1el2xp  33341  fmlasuc0  33346  elhf2  34477  findreccl  34642  rdgeqoa  35541  exrecfnlem  35550  finxpreclem4  35565  finxpreclem6  35567  harinf  40856  omssrncard  41147  nna1iscard  41152