ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eloni Unicode version

Theorem eloni 4158
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
StepHypRef Expression
1 elong 4156 . 2  |-  ( A  e.  On  ->  ( A  e.  On  <->  Ord  A ) )
21ibi 174 1  |-  ( A  e.  On  ->  Ord  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   Ord word 4145   Oncon0 4146
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2612  df-in 2988  df-ss 2995  df-uni 3622  df-tr 3896  df-iord 4149  df-on 4151
This theorem is referenced by:  elon2  4159  onelon  4167  onin  4169  onelss  4170  ontr1  4172  onordi  4209  onss  4265  suceloni  4273  sucelon  4275  onsucmin  4279  onsucelsucr  4280  onintonm  4289  ordsucunielexmid  4302  onsucuni2  4335  nnord  4380  tfrlem1  5977  tfrlemisucaccv  5994  tfrlemibfn  5997  tfrlemiubacc  5999  tfrexlem  6003  tfr1onlemsucfn  6009  tfr1onlemsucaccv  6010  tfr1onlembfn  6013  tfr1onlemubacc  6015  tfrcllemsucfn  6022  tfrcllemsucaccv  6023  tfrcllembfn  6026  tfrcllemubacc  6028  sucinc2  6110  phplem4on  6423  ordiso  6541
  Copyright terms: Public domain W3C validator