Theorem onordi 6475

Description: An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)

Hypothesis

Ref	Expression
on.1	⊢ 𝐴 ∈ On

Assertion

Ref	Expression
onordi	⊢ Ord 𝐴

Proof of Theorem onordi

Step	Hyp	Ref	Expression
1		on.1	. 2 ⊢ 𝐴 ∈ On
2		eloni 6371	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ord 𝐴

Syntax hints:   ∈ wcel 2149  Ord word 6360  Oncon0 6361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-ord 6364  df-on 6365

This theorem is referenced by:  onirri  6476  onsucssi  7836  ord1eln01  8480  ord2eln012  8481  oawordeulem  8538  omopthi  8646  en2  9239  en3  9240  ssttrcl  9683  ttrcltr  9684  dmttrcl  9689  ttrclselem2  9694  bndrank  9812  rankprb  9822  rankuniss  9837  rankelun  9843  rankelpr  9844  rankelop  9845  rankmapu  9849  rankxplim3  9852  rankxpsuc  9853  cardlim  9957  carduni  9966  dfac8b  10014  alephdom2  10070  alephfp  10091  dfac12lem2  10127  dju1p1e2ALT  10157  cfsmolem  10253  ttukeylem6  10497  ttukeylem7  10498  unsnen  10536  efgmnvl  19783  nogt01o  27825  cutbdaybnd2lim  27955  lesrec  27957  bday1  27972  cuteq1  27975  newbday  28060  negsproplem7  28192  mulsproplem13  28286  mulsproplem14  28287  ltonold  28419  addonbday  28437  bdaypw2n0bndlem  28621  z12bdaylem  28642  hfuni  36574  finxpsuclem  37930  pwfi2f1o  43714  nelsubc3  49733