Theorem onordi 6082

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

Syntax hints:   ∈ wcel 2107  Ord word 5977  Oncon0 5978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-in 3799  df-ss 3806  df-uni 4674  df-tr 4990  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-ord 5981  df-on 5982

This theorem is referenced by:  ontrci  6083  onirri  6084  onun2i  6093  onuniorsuci  7319  onsucssi  7321  oawordeulem  7920  omopthi  8023  bndrank  9003  rankprb  9013  rankuniss  9028  rankelun  9034  rankelpr  9035  rankelop  9036  rankmapu  9040  rankxplim3  9043  rankxpsuc  9044  cardlim  9133  carduni  9142  dfac8b  9189  alephdom2  9245  alephfp  9266  dfac12lem2  9303  pm110.643ALT  9337  cfsmolem  9429  ttukeylem6  9673  ttukeylem7  9674  unsnen  9712  efgmnvl  18515  slerec  32516  hfuni  32884  finxpsuclem  33832  pwfi2f1o  38635