Theorem onordi 6045

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

Syntax hints:   ∈ wcel 2157  Ord word 5940  Oncon0 5941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-v 3387  df-in 3776  df-ss 3783  df-uni 4629  df-tr 4946  df-po 5233  df-so 5234  df-fr 5271  df-we 5273  df-ord 5944  df-on 5945

This theorem is referenced by:  ontrci  6046  onirri  6047  onun2i  6056  onuniorsuci  7273  onsucssi  7275  oawordeulem  7874  omopthi  7977  bndrank  8954  rankprb  8964  rankuniss  8979  rankelun  8985  rankelpr  8986  rankelop  8987  rankmapu  8991  rankxplim3  8994  rankxpsuc  8995  cardlim  9084  carduni  9093  dfac8b  9140  alephdom2  9196  alephfp  9217  dfac12lem2  9254  pm110.643ALT  9288  cfsmolem  9380  ttukeylem6  9624  ttukeylem7  9625  unsnen  9663  efgmnvl  18440  slerec  32436  hfuni  32804  finxpsuclem  33732  pwfi2f1o  38451