Theorem onordi 6375

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

Syntax hints:   ∈ wcel 2107  Ord word 6269  Oncon0 6270

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-tr 5193  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-ord 6273  df-on 6274

This theorem is referenced by:  ontrci  6376  onirri  6377  onuniorsuci  7695  onsucssi  7697  ord1eln01  8335  ord2eln012  8336  oawordeulem  8394  omopthi  8500  ssttrcl  9482  ttrcltr  9483  dmttrcl  9488  ttrclselem2  9493  bndrank  9608  rankprb  9618  rankuniss  9633  rankelun  9639  rankelpr  9640  rankelop  9641  rankmapu  9645  rankxplim3  9648  rankxpsuc  9649  cardlim  9739  carduni  9748  dfac8b  9796  alephdom2  9852  alephfp  9873  dfac12lem2  9909  dju1p1e2ALT  9939  cfsmolem  10035  ttukeylem6  10279  ttukeylem7  10280  unsnen  10318  efgmnvl  19329  nogt01o  33908  scutbdaybnd2lim  34020  slerec  34022  bday1s  34034  newbday  34091  hfuni  34495  finxpsuclem  35577  pwfi2f1o  40928