Theorem onordi 6494

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

Syntax hints:   ∈ wcel 2107  Ord word 6382  Oncon0 6383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-ord 6386  df-on 6387

This theorem is referenced by:  onirri  6496  onsucssi  7863  ord1eln01  8535  ord2eln012  8536  oawordeulem  8593  omopthi  8700  en2  9316  en3  9317  ssttrcl  9756  ttrcltr  9757  dmttrcl  9762  ttrclselem2  9767  bndrank  9882  rankprb  9892  rankuniss  9907  rankelun  9913  rankelpr  9914  rankelop  9915  rankmapu  9919  rankxplim3  9922  rankxpsuc  9923  cardlim  10013  carduni  10022  dfac8b  10072  alephdom2  10128  alephfp  10149  dfac12lem2  10186  dju1p1e2ALT  10216  cfsmolem  10311  ttukeylem6  10555  ttukeylem7  10556  unsnen  10594  efgmnvl  19733  nogt01o  27742  scutbdaybnd2lim  27863  slerec  27865  bday1s  27877  cuteq1  27879  newbday  27941  negsproplem7  28067  mulsproplem13  28155  mulsproplem14  28156  sltonold  28284  pw2bday  28419  hfuni  36186  finxpsuclem  37399  pwfi2f1o  43113