Theorem onordi 4987

Description: An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)

Hypothesis

Ref	Expression
on.1

Assertion

Ref	Expression
onordi

Proof of Theorem onordi

Step	Hyp	Ref	Expression
1		on.1	. 2
2		eloni 4893	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  e.wcel 1818  Ordword 4882  con0 4883

This theorem is referenced by:  ontrci  4988  onirri  4989  onun2i  4998  onuniorsuci  6674  onsucssi  6676  oawordeulem  7222  omopthi  7325  bndrank  8280  rankprb  8290  rankuniss  8305  rankelun  8311  rankelpr  8312  rankelop  8313  rankmapu  8317  rankxplim3  8320  rankxpsuc  8321  cardlim  8374  carduni  8383  dfac8b  8433  alephdom2  8489  alephfp  8510  dfac12lem2  8545  pm110.643ALT  8579  cfsmolem  8671  ttukeylem6  8915  ttukeylem7  8916  unsnen  8949  mreexexd  15045  efgmnvl  16732  nodenselem4  29444  hfuni  29841  pwfi2f1o  31044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887