Theorem onordi 6433

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

Syntax hints:   ∈ wcel 2109  Ord word 6319  Oncon0 6320

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3446  df-ss 3928  df-uni 4868  df-tr 5210  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6323  df-on 6324

This theorem is referenced by:  onirri  6435  onsucssi  7797  ord1eln01  8437  ord2eln012  8438  oawordeulem  8495  omopthi  8602  en2  9202  en3  9203  ssttrcl  9644  ttrcltr  9645  dmttrcl  9650  ttrclselem2  9655  bndrank  9770  rankprb  9780  rankuniss  9795  rankelun  9801  rankelpr  9802  rankelop  9803  rankmapu  9807  rankxplim3  9810  rankxpsuc  9811  cardlim  9901  carduni  9910  dfac8b  9960  alephdom2  10016  alephfp  10037  dfac12lem2  10074  dju1p1e2ALT  10104  cfsmolem  10199  ttukeylem6  10443  ttukeylem7  10444  unsnen  10482  efgmnvl  19620  nogt01o  27584  scutbdaybnd2lim  27705  slerec  27707  bday1s  27719  cuteq1  27722  newbday  27789  negsproplem7  27916  mulsproplem13  28007  mulsproplem14  28008  sltonold  28138  hfuni  36145  finxpsuclem  37358  pwfi2f1o  43058  nelsubc3  49033