Theorem onordi 6428

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

Syntax hints:   ∈ wcel 2113  Ord word 6314  Oncon0 6315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-v 3440  df-ss 3916  df-uni 4862  df-tr 5204  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  onirri  6429  onsucssi  7781  ord1eln01  8421  ord2eln012  8422  oawordeulem  8479  omopthi  8587  en2  9178  en3  9179  ssttrcl  9622  ttrcltr  9623  dmttrcl  9628  ttrclselem2  9633  bndrank  9751  rankprb  9761  rankuniss  9776  rankelun  9782  rankelpr  9783  rankelop  9784  rankmapu  9788  rankxplim3  9791  rankxpsuc  9792  cardlim  9882  carduni  9891  dfac8b  9939  alephdom2  9995  alephfp  10016  dfac12lem2  10053  dju1p1e2ALT  10083  cfsmolem  10178  ttukeylem6  10422  ttukeylem7  10423  unsnen  10461  efgmnvl  19641  nogt01o  27662  scutbdaybnd2lim  27785  slerec  27787  bday1s  27802  cuteq1  27805  newbday  27874  negsproplem7  28003  mulsproplem13  28097  mulsproplem14  28098  sltonold  28229  bdaypw2n0s  28420  hfuni  36327  finxpsuclem  37541  pwfi2f1o  43280  nelsubc3  49258