Theorem onordi 6356

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

Syntax hints:   ∈ wcel 2108  Ord word 6250  Oncon0 6251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-tr 5188  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255

This theorem is referenced by:  ontrci  6357  onirri  6358  onuniorsuci  7661  onsucssi  7663  oawordeulem  8347  omopthi  8451  bndrank  9530  rankprb  9540  rankuniss  9555  rankelun  9561  rankelpr  9562  rankelop  9563  rankmapu  9567  rankxplim3  9570  rankxpsuc  9571  cardlim  9661  carduni  9670  dfac8b  9718  alephdom2  9774  alephfp  9795  dfac12lem2  9831  dju1p1e2ALT  9861  cfsmolem  9957  ttukeylem6  10201  ttukeylem7  10202  unsnen  10240  efgmnvl  19235  ssttrcl  33701  ttrcltr  33702  dmttrcl  33707  ttrclselem2  33712  nogt01o  33826  scutbdaybnd2lim  33938  slerec  33940  bday1s  33952  newbday  34009  hfuni  34413  finxpsuclem  35495  pwfi2f1o  40837