Theorem nnon 7857

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

Syntax hints:   → wi 4   ∈ wcel 2106  Oncon0 6361  ωcom 7851

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964  df-om 7852

This theorem is referenced by:  nnoni  7858  nnord  7859  peano4  7879  findsg  7886  onasuc  8524  onmsuc  8525  nna0  8600  nnm0  8601  nnasuc  8602  nnmsuc  8603  nnesuc  8604  nnecl  8609  nnawordi  8617  nnmword  8629  nnawordex  8633  nnaordex  8634  oaabslem  8642  oaabs  8643  oaabs2  8644  omabslem  8645  omabs  8646  nnneo  8650  nneob  8651  dif1ennn  9157  findcard2  9160  onfin2  9227  nndomo  9229  findcard3  9281  findcard3OLD  9282  dffi3  9422  card2inf  9546  elom3  9639  cantnfp1lem3  9671  cnfcomlem  9690  cnfcom  9691  cnfcom3  9695  ttrcltr  9707  ttrclselem1  9716  ttrclselem2  9717  finnum  9939  cardnn  9954  nnsdomel  9981  harsucnn  9989  nnadjuALT  10189  ficardun2  10193  ficardun2OLD  10194  ackbij1lem15  10225  ackbij2lem2  10231  ackbij2lem3  10232  ackbij2  10234  fin23lem22  10318  isf32lem5  10348  fin1a2lem4  10394  fin1a2lem9  10399  pwfseqlem3  10651  winainflem  10684  wunr1om  10710  tskr1om  10758  grothomex  10820  pion  10870  om2uzlt2i  13912  precsexlem3  27644  precsexlem4  27645  precsexlem5  27646  bnj168  33729  satfvsuc  34340  satf0suc  34355  sat1el2xp  34358  fmlasuc0  34363  elhf2  35135  findreccl  35326  rdgeqoa  36239  exrecfnlem  36248  finxpreclem4  36263  finxpreclem6  36265  harinf  41758  onexoegt  41978  oaabsb  42029  nnoeomeqom  42047  cantnfub  42056  dflim5  42064  onmcl  42066  omabs2  42067  tfsconcat0b  42081  naddcnffo  42099  naddonnn  42131  naddwordnexlem0  42132  naddwordnexlem3  42135  oawordex3  42136  naddwordnexlem4  42137  omssrncard  42276  nna1iscard  42281