Theorem onordi 6373

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

Syntax hints:   ∈ wcel 2106  Ord word 6267  Oncon0 6268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3433  df-in 3895  df-ss 3905  df-uni 4842  df-tr 5194  df-po 5505  df-so 5506  df-fr 5546  df-we 5548  df-ord 6271  df-on 6272

This theorem is referenced by:  ontrci  6374  onirri  6375  onuniorsuci  7686  onsucssi  7688  ord1eln01  8324  ord2eln012  8325  oawordeulem  8383  omopthi  8489  ssttrcl  9471  ttrcltr  9472  dmttrcl  9477  ttrclselem2  9482  bndrank  9597  rankprb  9607  rankuniss  9622  rankelun  9628  rankelpr  9629  rankelop  9630  rankmapu  9634  rankxplim3  9637  rankxpsuc  9638  cardlim  9728  carduni  9737  dfac8b  9785  alephdom2  9841  alephfp  9862  dfac12lem2  9898  dju1p1e2ALT  9928  cfsmolem  10024  ttukeylem6  10268  ttukeylem7  10269  unsnen  10307  efgmnvl  19318  nogt01o  33896  scutbdaybnd2lim  34008  slerec  34010  bday1s  34022  newbday  34079  hfuni  34483  finxpsuclem  35565  pwfi2f1o  40918