Theorem onordi 6445

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

Syntax hints:   ∈ wcel 2109  Ord word 6331  Oncon0 6332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-ss 3931  df-uni 4872  df-tr 5215  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  onirri  6447  onsucssi  7817  ord1eln01  8460  ord2eln012  8461  oawordeulem  8518  omopthi  8625  en2  9226  en3  9227  ssttrcl  9668  ttrcltr  9669  dmttrcl  9674  ttrclselem2  9679  bndrank  9794  rankprb  9804  rankuniss  9819  rankelun  9825  rankelpr  9826  rankelop  9827  rankmapu  9831  rankxplim3  9834  rankxpsuc  9835  cardlim  9925  carduni  9934  dfac8b  9984  alephdom2  10040  alephfp  10061  dfac12lem2  10098  dju1p1e2ALT  10128  cfsmolem  10223  ttukeylem6  10467  ttukeylem7  10468  unsnen  10506  efgmnvl  19644  nogt01o  27608  scutbdaybnd2lim  27729  slerec  27731  bday1s  27743  cuteq1  27746  newbday  27813  negsproplem7  27940  mulsproplem13  28031  mulsproplem14  28032  sltonold  28162  hfuni  36172  finxpsuclem  37385  pwfi2f1o  43085  nelsubc3  49057