Theorem onordi 5832

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

Syntax hints:   ∈ wcel 1990  Ord word 5722  Oncon0 5723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727

This theorem is referenced by:  ontrci  5833  onirri  5834  onun2i  5843  onuniorsuci  7039  onsucssi  7041  oawordeulem  7634  omopthi  7737  bndrank  8704  rankprb  8714  rankuniss  8729  rankelun  8735  rankelpr  8736  rankelop  8737  rankmapu  8741  rankxplim3  8744  rankxpsuc  8745  cardlim  8798  carduni  8807  dfac8b  8854  alephdom2  8910  alephfp  8931  dfac12lem2  8966  pm110.643ALT  9000  cfsmolem  9092  ttukeylem6  9336  ttukeylem7  9337  unsnen  9375  mreexexdOLD  16309  efgmnvl  18127  slerec  31923  hfuni  32291  finxpsuclem  33234  pwfi2f1o  37666