Theorem onordi 6474

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

Syntax hints:   ∈ wcel 2099  Ord word 6362  Oncon0 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-v 3471  df-in 3951  df-ss 3961  df-uni 4904  df-tr 5260  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-ord 6366  df-on 6367

This theorem is referenced by:  onirri  6476  onsucssi  7839  ord1eln01  8510  ord2eln012  8511  oawordeulem  8568  omopthi  8675  en2  9297  en3  9298  ssttrcl  9730  ttrcltr  9731  dmttrcl  9736  ttrclselem2  9741  bndrank  9856  rankprb  9866  rankuniss  9881  rankelun  9887  rankelpr  9888  rankelop  9889  rankmapu  9893  rankxplim3  9896  rankxpsuc  9897  cardlim  9987  carduni  9996  dfac8b  10046  alephdom2  10102  alephfp  10123  dfac12lem2  10159  dju1p1e2ALT  10189  cfsmolem  10285  ttukeylem6  10529  ttukeylem7  10530  unsnen  10568  efgmnvl  19660  nogt01o  27616  scutbdaybnd2lim  27737  slerec  27739  bday1s  27751  cuteq1  27753  newbday  27815  negsproplem7  27933  mulsproplem13  28015  mulsproplem14  28016  sltonold  28140  hfuni  35716  finxpsuclem  36812  pwfi2f1o  42442