Theorem onordi 6423

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

Syntax hints:   ∈ wcel 2119  Ord word 6309  Oncon0 6310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-v 3433  df-ss 3900  df-uni 4839  df-tr 5180  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-ord 6313  df-on 6314

This theorem is referenced by:  onirri  6424  onsucssi  7781  ord1eln01  8421  ord2eln012  8422  oawordeulem  8479  omopthi  8587  en2  9180  en3  9181  ssttrcl  9627  ttrcltr  9628  dmttrcl  9633  ttrclselem2  9638  bndrank  9756  rankprb  9766  rankuniss  9781  rankelun  9787  rankelpr  9788  rankelop  9789  rankmapu  9793  rankxplim3  9796  rankxpsuc  9797  cardlim  9887  carduni  9896  dfac8b  9944  alephdom2  10000  alephfp  10021  dfac12lem2  10058  dju1p1e2ALT  10088  cfsmolem  10183  ttukeylem6  10427  ttukeylem7  10428  unsnen  10466  efgmnvl  19680  nogt01o  27678  cutbdaybnd2lim  27807  lesrec  27809  bday1  27824  cuteq1  27827  newbday  27912  negsproplem7  28044  mulsproplem13  28138  mulsproplem14  28139  ltonold  28271  addonbday  28289  bdaypw2n0bndlem  28473  z12bdaylem  28494  hfuni  36412  finxpsuclem  37759  pwfi2f1o  43541  nelsubc3  49561