Theorem onordi 6295

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

Syntax hints:   ∈ wcel 2114  Ord word 6190  Oncon0 6191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3496  df-in 3943  df-ss 3952  df-uni 4839  df-tr 5173  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195

This theorem is referenced by:  ontrci  6296  onirri  6297  onun2i  6306  onuniorsuci  7554  onsucssi  7556  oawordeulem  8180  omopthi  8284  bndrank  9270  rankprb  9280  rankuniss  9295  rankelun  9301  rankelpr  9302  rankelop  9303  rankmapu  9307  rankxplim3  9310  rankxpsuc  9311  cardlim  9401  carduni  9410  dfac8b  9457  alephdom2  9513  alephfp  9534  dfac12lem2  9570  dju1p1e2ALT  9600  cfsmolem  9692  ttukeylem6  9936  ttukeylem7  9937  unsnen  9975  efgmnvl  18840  slerec  33277  hfuni  33645  finxpsuclem  34681  pwfi2f1o  39716