Theorem onordi 6459

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

Syntax hints:   ∈ wcel 2142  Ord word 6345  Oncon0 6346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-v 3456  df-ss 3921  df-uni 4866  df-tr 5208  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349  df-on 6350

This theorem is referenced by:  onirri  6460  onsucssi  7821  ord1eln01  8465  ord2eln012  8466  oawordeulem  8523  omopthi  8631  en2  9224  en3  9225  ssttrcl  9670  ttrcltr  9671  dmttrcl  9676  ttrclselem2  9681  bndrank  9799  rankprb  9809  rankuniss  9824  rankelun  9830  rankelpr  9831  rankelop  9832  rankmapu  9836  rankxplim3  9839  rankxpsuc  9840  cardlim  9930  carduni  9939  dfac8b  9987  alephdom2  10043  alephfp  10064  dfac12lem2  10101  dju1p1e2ALT  10131  cfsmolem  10227  ttukeylem6  10471  ttukeylem7  10472  unsnen  10510  efgmnvl  19754  nogt01o  27757  cutbdaybnd2lim  27887  lesrec  27889  bday1  27904  cuteq1  27907  newbday  27992  negsproplem7  28124  mulsproplem13  28218  mulsproplem14  28219  ltonold  28351  addonbday  28369  bdaypw2n0bndlem  28553  z12bdaylem  28574  hfuni  36531  finxpsuclem  37888  pwfi2f1o  43670  nelsubc3  49689