Theorem onordi 6296

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 2112  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 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-v 3400  df-in 3860  df-ss 3870  df-uni 4806  df-tr 5147  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-ord 6194  df-on 6195

This theorem is referenced by:  ontrci  6297  onirri  6298  onuniorsuci  7596  onsucssi  7598  oawordeulem  8260  omopthi  8364  bndrank  9422  rankprb  9432  rankuniss  9447  rankelun  9453  rankelpr  9454  rankelop  9455  rankmapu  9459  rankxplim3  9462  rankxpsuc  9463  cardlim  9553  carduni  9562  dfac8b  9610  alephdom2  9666  alephfp  9687  dfac12lem2  9723  dju1p1e2ALT  9753  cfsmolem  9849  ttukeylem6  10093  ttukeylem7  10094  unsnen  10132  efgmnvl  19058  nogt01o  33585  scutbdaybnd2lim  33697  slerec  33699  bday1s  33711  newbday  33768  hfuni  34172  finxpsuclem  35254  pwfi2f1o  40565