Theorem onordi 6420

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

Syntax hints:   ∈ wcel 2109  Ord word 6306  Oncon0 6307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-ss 3920  df-uni 4859  df-tr 5200  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  onirri  6421  onsucssi  7774  ord1eln01  8414  ord2eln012  8415  oawordeulem  8472  omopthi  8579  en2  9169  en3  9170  ssttrcl  9611  ttrcltr  9612  dmttrcl  9617  ttrclselem2  9622  bndrank  9737  rankprb  9747  rankuniss  9762  rankelun  9768  rankelpr  9769  rankelop  9770  rankmapu  9774  rankxplim3  9777  rankxpsuc  9778  cardlim  9868  carduni  9877  dfac8b  9925  alephdom2  9981  alephfp  10002  dfac12lem2  10039  dju1p1e2ALT  10069  cfsmolem  10164  ttukeylem6  10408  ttukeylem7  10409  unsnen  10447  efgmnvl  19593  nogt01o  27606  scutbdaybnd2lim  27728  slerec  27730  bday1s  27745  cuteq1  27748  newbday  27816  negsproplem7  27945  mulsproplem13  28036  mulsproplem14  28037  sltonold  28167  hfuni  36158  finxpsuclem  37371  pwfi2f1o  43069  nelsubc3  49056