Theorem onordi 6479

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

This proof depends on syntax axioms:   ∈ wcel 2144  Ord word 6364  Oncon0 6365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3897  df-uni 4867  df-tr 5212  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369

This theorem is used by:  onirri  6480  onsucssi  7856  ord1eln01  8511  ord2eln012  8512  oawordeulem  8569  omopthi  8677  en2  9278  en3  9279  ssttrcl  9723  ttrcltr  9724  dmttrcl  9729  ttrclselem2  9734  bndrank  9861  rankprb  9872  rankuniss  9890  rankelun  9896  rankelpr  9897  rankelop  9898  rankmapu  9902  rankxplim3  9905  rankxpsuc  9906  hfuniOLD  9932  cardlim  10060  carduni  10069  dfac8b  10117  alephdom2  10173  alephfp  10194  dfac12lem2  10230  dju1p1e2ALT  10260  cfsmolem  10355  ttukeylem6  10599  ttukeylem7  10600  unsnen  10644  efgmnvl  19937  nogt01o  28062  cutbdaybnd2lim  28192  lesrec  28194  bday1  28209  cuteq1  28212  newbday  28297  negsproplem7  28429  mulsproplem13  28523  mulsproplem14  28524  ltonold  28656  addonbday  28674  bdaypw2n0bndlem  28858  z12bdaylem  28879  rankscottu  35811  finxpsuclem  38429  findcard4  38741  pwfi2f1o  44207  nelsubc3  50293