Theorem onordi 6471

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

This proof depends on syntax axioms:   ∈ wcel 2145  Ord word 6356  Oncon0 6357

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6360  df-on 6361

This theorem is used by:  onirri  6472  onsucssi  7837  ord1eln01  8483  ord2eln012  8484  oawordeulem  8541  omopthi  8649  en2  9250  en3  9251  ssttrcl  9694  ttrcltr  9695  dmttrcl  9700  ttrclselem2  9705  bndrank  9823  rankprb  9833  rankuniss  9848  rankelun  9854  rankelpr  9855  rankelop  9856  rankmapu  9860  rankxplim3  9863  rankxpsuc  9864  cardlim  9977  carduni  9986  dfac8b  10034  alephdom2  10090  alephfp  10111  dfac12lem2  10147  dju1p1e2ALT  10177  cfsmolem  10272  ttukeylem6  10516  ttukeylem7  10517  unsnen  10561  efgmnvl  19841  nogt01o  27932  cutbdaybnd2lim  28062  lesrec  28064  bday1  28079  cuteq1  28082  newbday  28167  negsproplem7  28299  mulsproplem13  28393  mulsproplem14  28394  ltonold  28526  addonbday  28544  bdaypw2n0bndlem  28728  z12bdaylem  28749  rankscottu  35636  hfuni  36764  finxpsuclem  38151  findcard4  38463  pwfi2f1o  43937  nelsubc3  49997