Theorem nnon 7861

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

Syntax hints:   → wi 4   ∈ wcel 2107  Oncon0 6365  ωcom 7855

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-om 7856

This theorem is referenced by:  nnoni  7862  nnord  7863  peano4  7883  findsg  7890  onasuc  8528  onmsuc  8529  nna0  8604  nnm0  8605  nnasuc  8606  nnmsuc  8607  nnesuc  8608  nnecl  8613  nnawordi  8621  nnmword  8633  nnawordex  8637  nnaordex  8638  oaabslem  8646  oaabs  8647  oaabs2  8648  omabslem  8649  omabs  8650  nnneo  8654  nneob  8655  dif1ennn  9161  findcard2  9164  onfin2  9231  nndomo  9233  findcard3  9285  findcard3OLD  9286  dffi3  9426  card2inf  9550  elom3  9643  cantnfp1lem3  9675  cnfcomlem  9694  cnfcom  9695  cnfcom3  9699  ttrcltr  9711  ttrclselem1  9720  ttrclselem2  9721  finnum  9943  cardnn  9958  nnsdomel  9985  harsucnn  9993  nnadjuALT  10193  ficardun2  10197  ficardun2OLD  10198  ackbij1lem15  10229  ackbij2lem2  10235  ackbij2lem3  10236  ackbij2  10238  fin23lem22  10322  isf32lem5  10352  fin1a2lem4  10398  fin1a2lem9  10403  pwfseqlem3  10655  winainflem  10688  wunr1om  10714  tskr1om  10762  grothomex  10824  pion  10874  om2uzlt2i  13916  precsexlem3  27655  precsexlem4  27656  precsexlem5  27657  bnj168  33741  satfvsuc  34352  satf0suc  34367  sat1el2xp  34370  fmlasuc0  34375  elhf2  35147  findreccl  35338  rdgeqoa  36251  exrecfnlem  36260  finxpreclem4  36275  finxpreclem6  36277  harinf  41773  onexoegt  41993  oaabsb  42044  nnoeomeqom  42062  cantnfub  42071  dflim5  42079  onmcl  42081  omabs2  42082  tfsconcat0b  42096  naddcnffo  42114  naddonnn  42146  naddwordnexlem0  42147  naddwordnexlem3  42150  oawordex3  42151  naddwordnexlem4  42152  omssrncard  42291  nna1iscard  42296