Theorem onordi 6430

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

Syntax hints:   ∈ wcel 2113  Ord word 6316  Oncon0 6317

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321

This theorem is referenced by:  onirri  6431  onsucssi  7783  ord1eln01  8423  ord2eln012  8424  oawordeulem  8481  omopthi  8589  en2  9180  en3  9181  ssttrcl  9624  ttrcltr  9625  dmttrcl  9630  ttrclselem2  9635  bndrank  9753  rankprb  9763  rankuniss  9778  rankelun  9784  rankelpr  9785  rankelop  9786  rankmapu  9790  rankxplim3  9793  rankxpsuc  9794  cardlim  9884  carduni  9893  dfac8b  9941  alephdom2  9997  alephfp  10018  dfac12lem2  10055  dju1p1e2ALT  10085  cfsmolem  10180  ttukeylem6  10424  ttukeylem7  10425  unsnen  10463  efgmnvl  19643  nogt01o  27664  cutbdaybnd2lim  27793  lesrec  27795  bday1  27810  cuteq1  27813  newbday  27898  negsproplem7  28030  mulsproplem13  28124  mulsproplem14  28125  ltonold  28257  addonbday  28275  bdaypw2n0bndlem  28459  z12bdaylem  28480  hfuni  36378  finxpsuclem  37602  pwfi2f1o  43338  nelsubc3  49316