Theorem eloni 4472

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
eloni	|- ( A e. On -> Ord A )

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 4470	. 2 |- ( A e. On -> ( A e. On <-> Ord A ) )
2	1	ibi 176	1 |- ( A e. On -> Ord A )

Syntax hints:   -> wi 4   e. wcel 2202   Ord word 4459   Oncon0 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-in 3206  df-ss 3213  df-uni 3894  df-tr 4188  df-iord 4463  df-on 4465

This theorem is referenced by:  elon2  4473  onelon  4481  onin  4483  onelss  4484  ontr1  4486  onordi  4523  onss  4591  onsuc  4599  onsucb  4601  onsucmin  4605  onsucelsucr  4606  onintonm  4615  ordsucunielexmid  4629  onsucuni2  4662  nnord  4710  tfrlem1  6473  tfrlemisucaccv  6490  tfrlemibfn  6493  tfrlemiubacc  6495  tfrexlem  6499  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembfn  6509  tfr1onlemubacc  6511  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembfn  6522  tfrcllemubacc  6524  sucinc2  6613  phplem4on  7053  ordiso  7234