Theorem eloni 6261

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

Assertion

Ref	Expression
eloni	⊢ (𝐴 ∈ On → Ord 𝐴)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 6259	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 266	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2108  Ord word 6250  Oncon0 6251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-tr 5188  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255

This theorem is referenced by:  onelon  6276  onin  6282  ontri1  6285  onfr  6290  onelpss  6291  onsseleq  6292  onelss  6293  ontr1  6297  ontr2  6298  ordunidif  6299  on0eln0  6306  ordsssuc  6337  onsssuc  6338  onnbtwn  6342  suc11  6354  onun2  6355  onordi  6356  onssneli  6361  epweon  7603  ordeleqon  7609  onss  7611  ordsuc  7636  onpwsuc  7638  onpsssuc  7641  onsucmin  7643  ordunpr  7648  ordunisuc  7654  onsucuni2  7656  onuninsuci  7662  ordunisuc2  7666  ordzsl  7667  onzsl  7668  nlimon  7673  tfinds  7681  tfindsg2  7683  nnord  7695  onfununi  8143  smo11  8166  smoord  8167  smoword  8168  smogt  8169  tfrlem1  8178  tfrlem9a  8188  tfrlem15  8194  tz7.44-2  8209  tz7.48lem  8242  oe0m1  8313  oaordi  8339  oaord  8340  oacan  8341  oawordri  8343  oalimcl  8353  oaass  8354  omord2  8360  omcan  8362  omwordi  8364  omword1  8366  omword2  8367  om00  8368  omlimcl  8371  omass  8373  omeulem2  8376  omopth2  8377  oen0  8379  oeord  8381  oecan  8382  oewordi  8384  oeworde  8386  oelimcl  8393  oeeulem  8394  oeeui  8395  nnarcl  8409  nnawordi  8414  nnawordex  8430  oaabs2  8439  omabs  8441  omsmo  8448  omxpenlem  8813  infensuc  8891  nndomog  8904  onomeneq  8943  ordiso  9205  ordtypelem2  9208  hartogslem1  9231  cantnflt  9360  cantnfp1lem3  9368  cantnfp1  9369  oemapso  9370  oemapvali  9372  cantnflem1d  9376  cantnflem1  9377  cantnf  9381  oemapwe  9382  cantnffval2  9383  cnfcom  9388  r111  9464  r1ordg  9467  rankonidlem  9517  bndrank  9530  r1pw  9534  r1pwALT  9535  rankbnd2  9558  tcrank  9573  cardprclem  9668  carduni  9670  cardmin2  9688  infxpenlem  9700  alephdom  9768  alephdom2  9774  cardaleph  9776  iscard3  9780  alephfp  9795  dfac12lem1  9830  dfac12lem2  9831  dfac12lem3  9832  cflim2  9950  cofsmo  9956  cfsmolem  9957  coftr  9960  cfcof  9961  fin67  10082  hsmexlem5  10117  zorn2lem6  10188  ttukeylem3  10198  ttukeylem5  10200  ttukeylem6  10201  ttukeylem7  10202  winainflem  10380  r1limwun  10423  r1wunlim  10424  tsksuc  10449  inar1  10462  gruina  10505  grur1a  10506  grur1  10507  onunel  33592  dfrdg2  33677  poseq  33729  soseq  33730  naddcllem  33758  nodmord  33783  noextendseq  33797  noextenddif  33798  nosupno  33833  nosupbday  33835  nosupres  33837  noinfno  33848  noinfbday  33850  noinfres  33852  noetasuplem4  33866  noetainflem4  33870  newbday  34009  ontgval  34547  ontgsucval  34548  onsuctopon  34550  onintopssconn  34556  onsuct0  34557  sucneqond  35463  onsucuni3  35465  aomclem4  40798  aomclem5  40799  dfsucon  41028  onfrALTlem3  42053  onfrALTlem2  42055  onfrALTlem3VD  42396  onfrALTlem2VD  42398  onsetreclem3  46298