Theorem onordi 6506

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

Syntax hints:   ∈ wcel 2108  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  onirri  6508  onsucssi  7878  ord1eln01  8552  ord2eln012  8553  oawordeulem  8610  omopthi  8717  en2  9343  en3  9344  ssttrcl  9784  ttrcltr  9785  dmttrcl  9790  ttrclselem2  9795  bndrank  9910  rankprb  9920  rankuniss  9935  rankelun  9941  rankelpr  9942  rankelop  9943  rankmapu  9947  rankxplim3  9950  rankxpsuc  9951  cardlim  10041  carduni  10050  dfac8b  10100  alephdom2  10156  alephfp  10177  dfac12lem2  10214  dju1p1e2ALT  10244  cfsmolem  10339  ttukeylem6  10583  ttukeylem7  10584  unsnen  10622  efgmnvl  19756  nogt01o  27759  scutbdaybnd2lim  27880  slerec  27882  bday1s  27894  cuteq1  27896  newbday  27958  negsproplem7  28084  mulsproplem13  28172  mulsproplem14  28173  sltonold  28301  pw2bday  28436  hfuni  36148  finxpsuclem  37363  pwfi2f1o  43053