Theorem onordi 6475

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

This proof depends on syntax axioms:   ∈ wcel 2145  Ord word 6360  Oncon0 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6364  df-on 6365

This theorem is used by:  onirri  6476  onsucssi  7850  ord1eln01  8497  ord2eln012  8498  oawordeulem  8555  omopthi  8663  en2  9264  en3  9265  ssttrcl  9709  ttrcltr  9710  dmttrcl  9715  ttrclselem2  9720  bndrank  9847  rankprb  9858  rankuniss  9876  rankelun  9882  rankelpr  9883  rankelop  9884  rankmapu  9888  rankxplim3  9891  rankxpsuc  9892  hfuniOLD  9918  cardlim  10046  carduni  10055  dfac8b  10103  alephdom2  10159  alephfp  10180  dfac12lem2  10216  dju1p1e2ALT  10246  cfsmolem  10341  ttukeylem6  10585  ttukeylem7  10586  unsnen  10630  efgmnvl  19921  nogt01o  28046  cutbdaybnd2lim  28176  lesrec  28178  bday1  28193  cuteq1  28196  newbday  28281  negsproplem7  28413  mulsproplem13  28507  mulsproplem14  28508  ltonold  28640  addonbday  28658  bdaypw2n0bndlem  28842  z12bdaylem  28863  rankscottu  35741  finxpsuclem  38300  findcard4  38612  pwfi2f1o  44082  nelsubc3  50148