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 6374	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
3	1, 2	ax-mp 5	1 ⊢ Ord 𝐴

Syntax hints:   ∈ wcel 2105  Ord word 6363  Oncon0 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-ord 6367  df-on 6368

This theorem is referenced by:  onirri  6477  onsucssi  7834  ord1eln01  8502  ord2eln012  8503  oawordeulem  8560  omopthi  8666  en2  9287  en3  9288  ssttrcl  9716  ttrcltr  9717  dmttrcl  9722  ttrclselem2  9727  bndrank  9842  rankprb  9852  rankuniss  9867  rankelun  9873  rankelpr  9874  rankelop  9875  rankmapu  9879  rankxplim3  9882  rankxpsuc  9883  cardlim  9973  carduni  9982  dfac8b  10032  alephdom2  10088  alephfp  10109  dfac12lem2  10145  dju1p1e2ALT  10175  cfsmolem  10271  ttukeylem6  10515  ttukeylem7  10516  unsnen  10554  efgmnvl  19630  nogt01o  27542  scutbdaybnd2lim  27663  slerec  27665  bday1s  27677  cuteq1  27679  newbday  27741  negsproplem7  27859  mulsproplem13  27941  mulsproplem14  27942  sltonold  28066  hfuni  35626  finxpsuclem  36742  pwfi2f1o  42301