Theorem nnon 7305

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

Syntax hints:   → wi 4   ∈ wcel 2157  Oncon0 5941  ωcom 7299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pr 5097  ax-un 7183

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-tr 4946  df-eprel 5225  df-po 5233  df-so 5234  df-fr 5271  df-we 5273  df-ord 5944  df-on 5945  df-lim 5946  df-suc 5947  df-om 7300

This theorem is referenced by:  nnoni  7306  nnord  7307  peano4  7322  findsg  7327  onasuc  7848  onmsuc  7849  nna0  7924  nnm0  7925  nnasuc  7926  nnmsuc  7927  nnesuc  7928  nnecl  7933  nnawordi  7941  nnmword  7953  nnawordex  7957  nnaordex  7958  oaabslem  7963  oaabs  7964  oaabs2  7965  omabslem  7966  omabs  7967  nnneo  7971  nneob  7972  onfin2  8394  findcard3  8445  dffi3  8579  card2inf  8702  elom3  8795  cantnfp1lem3  8827  cnfcomlem  8846  cnfcom  8847  cnfcom3  8851  finnum  9060  cardnn  9075  nnsdomel  9102  nnacda  9311  ficardun2  9313  ackbij1lem15  9344  ackbij2lem2  9350  ackbij2lem3  9351  ackbij2  9353  fin23lem22  9437  isf32lem5  9467  fin1a2lem4  9513  fin1a2lem9  9518  pwfseqlem3  9770  winainflem  9803  wunr1om  9829  tskr1om  9877  grothomex  9939  pion  9989  om2uzlt2i  13005  bnj168  31316  elhf2  32795  findreccl  32960  rdgeqoa  33716  finxpreclem4  33729  finxpreclem6  33731  harinf  38386