Theorem onordi 6478

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 𝐴

This proof depends on syntax axioms:   ∈ wcel 2146  Ord word 6363  Oncon0 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368

This theorem is used by:  onirri  6479  onsucssi  7843  ord1eln01  8487  ord2eln012  8488  oawordeulem  8545  omopthi  8653  en2  9247  en3  9248  ssttrcl  9691  ttrcltr  9692  dmttrcl  9697  ttrclselem2  9702  bndrank  9820  rankprb  9830  rankuniss  9845  rankelun  9851  rankelpr  9852  rankelop  9853  rankmapu  9857  rankxplim3  9860  rankxpsuc  9861  cardlim  9974  carduni  9983  dfac8b  10031  alephdom2  10087  alephfp  10108  dfac12lem2  10144  dju1p1e2ALT  10174  cfsmolem  10269  ttukeylem6  10513  ttukeylem7  10514  unsnen  10552  efgmnvl  19828  nogt01o  27911  cutbdaybnd2lim  28041  lesrec  28043  bday1  28058  cuteq1  28061  newbday  28146  negsproplem7  28278  mulsproplem13  28372  mulsproplem14  28373  ltonold  28505  addonbday  28523  bdaypw2n0bndlem  28707  z12bdaylem  28728  rankscottu  35580  hfuni  36713  finxpsuclem  38100  findcard4  38422  pwfi2f1o  43881  nelsubc3  49906