Theorem onordi 6470

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

Syntax hints:   ∈ wcel 2109  Ord word 6356  Oncon0 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-v 3466  df-ss 3948  df-uni 4889  df-tr 5235  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-ord 6360  df-on 6361

This theorem is referenced by:  onirri  6472  onsucssi  7841  ord1eln01  8513  ord2eln012  8514  oawordeulem  8571  omopthi  8678  en2  9292  en3  9293  ssttrcl  9734  ttrcltr  9735  dmttrcl  9740  ttrclselem2  9745  bndrank  9860  rankprb  9870  rankuniss  9885  rankelun  9891  rankelpr  9892  rankelop  9893  rankmapu  9897  rankxplim3  9900  rankxpsuc  9901  cardlim  9991  carduni  10000  dfac8b  10050  alephdom2  10106  alephfp  10127  dfac12lem2  10164  dju1p1e2ALT  10194  cfsmolem  10289  ttukeylem6  10533  ttukeylem7  10534  unsnen  10572  efgmnvl  19700  nogt01o  27665  scutbdaybnd2lim  27786  slerec  27788  bday1s  27800  cuteq1  27803  newbday  27870  negsproplem7  27997  mulsproplem13  28088  mulsproplem14  28089  sltonold  28219  hfuni  36207  finxpsuclem  37420  pwfi2f1o  43087  nelsubc3  49005