Theorem onordi 6497

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

Syntax hints:   ∈ wcel 2106  Ord word 6385  Oncon0 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-v 3480  df-ss 3980  df-uni 4913  df-tr 5266  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390

This theorem is referenced by:  onirri  6499  onsucssi  7862  ord1eln01  8533  ord2eln012  8534  oawordeulem  8591  omopthi  8698  en2  9313  en3  9314  ssttrcl  9753  ttrcltr  9754  dmttrcl  9759  ttrclselem2  9764  bndrank  9879  rankprb  9889  rankuniss  9904  rankelun  9910  rankelpr  9911  rankelop  9912  rankmapu  9916  rankxplim3  9919  rankxpsuc  9920  cardlim  10010  carduni  10019  dfac8b  10069  alephdom2  10125  alephfp  10146  dfac12lem2  10183  dju1p1e2ALT  10213  cfsmolem  10308  ttukeylem6  10552  ttukeylem7  10553  unsnen  10591  efgmnvl  19747  nogt01o  27756  scutbdaybnd2lim  27877  slerec  27879  bday1s  27891  cuteq1  27893  newbday  27955  negsproplem7  28081  mulsproplem13  28169  mulsproplem14  28170  sltonold  28298  pw2bday  28433  hfuni  36166  finxpsuclem  37380  pwfi2f1o  43085