Theorem nnon 7628

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

Syntax hints:   → wi 4   ∈ wcel 2112  Oncon0 6191  ωcom 7622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870  df-om 7623

This theorem is referenced by:  nnoni  7629  nnord  7630  peano4  7648  findsg  7655  onasuc  8233  onmsuc  8234  nna0  8310  nnm0  8311  nnasuc  8312  nnmsuc  8313  nnesuc  8314  nnecl  8319  nnawordi  8327  nnmword  8339  nnawordex  8343  nnaordex  8344  oaabslem  8350  oaabs  8351  oaabs2  8352  omabslem  8353  omabs  8354  nnneo  8358  nneob  8359  onfin2  8847  nndomo  8849  findcard3  8892  dffi3  9025  card2inf  9149  elom3  9241  cantnfp1lem3  9273  cnfcomlem  9292  cnfcom  9293  cnfcom3  9297  finnum  9529  cardnn  9544  nnsdomel  9571  harsucnn  9579  nnadjuALT  9777  ficardun2  9781  ficardun2OLD  9782  ackbij1lem15  9813  ackbij2lem2  9819  ackbij2lem3  9820  ackbij2  9822  fin23lem22  9906  isf32lem5  9936  fin1a2lem4  9982  fin1a2lem9  9987  pwfseqlem3  10239  winainflem  10272  wunr1om  10298  tskr1om  10346  grothomex  10408  pion  10458  om2uzlt2i  13489  bnj168  32375  satfvsuc  32990  satf0suc  33005  sat1el2xp  33008  fmlasuc0  33013  elhf2  34163  findreccl  34328  rdgeqoa  35227  exrecfnlem  35236  finxpreclem4  35251  finxpreclem6  35253  harinf  40500