Theorem eloni 6316

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 6314	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 267	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111  Ord word 6305  Oncon0 6306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-ss 3919  df-uni 4860  df-tr 5199  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-ord 6309  df-on 6310

This theorem is referenced by:  onelon  6331  onin  6337  ontri1  6340  onfr  6345  onelpss  6346  onsseleq  6347  onelss  6348  oneltri  6349  ontr1  6353  ontr2  6354  ordunidif  6356  on0eln0  6363  ordsssuc  6397  onsssuc  6398  onnbtwn  6402  onunel  6413  suc11  6415  onun2  6416  ontr  6417  onordi  6419  onssneli  6423  epweon  7708  epweonALT  7709  ordeleqon  7715  onss  7718  sucexeloni  7742  onpwsuc  7746  onpsssuc  7749  onsucmin  7751  ordunpr  7756  ordunisuc  7762  onsucuni2  7764  onuniorsuc  7767  ordunisuc2  7774  ordzsl  7775  onzsl  7776  nlimon  7781  tfinds  7790  tfindsg2  7792  nnord  7804  poseq  8088  soseq  8089  onfununi  8261  smo11  8284  smoord  8285  smoword  8286  smogt  8287  tfrlem1  8295  tfrlem9a  8305  tfrlem15  8311  tz7.44-2  8326  tz7.48lem  8360  ord3  8400  oe0m1  8436  oaordi  8461  oaord  8462  oacan  8463  oawordri  8465  oalimcl  8475  oaass  8476  omord2  8482  omcan  8484  omwordi  8486  omword1  8488  omword2  8489  om00  8490  omlimcl  8493  omass  8495  omeulem2  8498  omopth2  8499  oen0  8501  oeord  8503  oecan  8504  oewordi  8506  oeworde  8508  oelimcl  8515  oeeulem  8516  oeeui  8517  nnarcl  8531  nnawordi  8536  nnawordex  8552  oaabs2  8564  omabs  8566  omsmo  8573  cofonr  8589  naddcllem  8591  naddsuc2  8616  omxpenlem  8991  infensuc  9068  dif1enlem  9069  nndomog  9122  onomeneq  9123  ordiso  9402  ordtypelem2  9405  hartogslem1  9428  cantnflt  9562  cantnfp1lem3  9570  cantnfp1  9571  oemapso  9572  oemapvali  9574  cantnflem1d  9578  cantnflem1  9579  cantnf  9583  oemapwe  9584  cantnffval2  9585  cnfcom  9590  r111  9665  r1ordg  9668  rankonidlem  9718  bndrank  9731  r1pw  9735  r1pwALT  9736  rankbnd2  9759  tcrank  9774  cardprclem  9869  carduni  9871  cardmin2  9889  infxpenlem  9901  alephdom  9969  alephdom2  9975  cardaleph  9977  iscard3  9981  alephfp  9996  dfac12lem1  10032  dfac12lem2  10033  dfac12lem3  10034  cflim2  10151  cofsmo  10157  cfsmolem  10158  coftr  10161  cfcof  10162  fin67  10283  hsmexlem5  10318  zorn2lem6  10389  ttukeylem3  10399  ttukeylem5  10401  ttukeylem6  10402  ttukeylem7  10403  winainflem  10581  r1limwun  10624  r1wunlim  10625  tsksuc  10650  inar1  10663  gruina  10706  grur1a  10707  grur1  10708  nodmord  27590  noextendseq  27604  noextenddif  27605  nosupno  27640  nosupbday  27642  nosupres  27644  noinfno  27655  noinfbday  27657  noinfres  27659  noetasuplem4  27673  noetainflem4  27677  newbday  27845  fineqvnttrclse  35132  dfrdg2  35828  ontgval  36464  ontgsucval  36465  onsuctopon  36467  onintopssconn  36473  onsuct0  36474  sucneqond  37398  onsucuni3  37400  aomclem4  43089  aomclem5  43090  onintunirab  43259  omlimcl2  43274  onelord  43283  ordeldifsucon  43291  ordeldif1o  43292  onsucss  43298  onsucf1olem  43302  onov0suclim  43306  oe0rif  43317  onsucwordi  43320  oege1  43338  cantnfresb  43356  omabs2  43364  ordsssucb  43367  tfsconcatlem  43368  tfsconcatfv2  43372  tfsconcatrn  43374  tfsconcatb0  43376  tfsconcat0b  43378  tfsconcatrev  43380  onsucunipr  43404  oaun3lem1  43406  oaun3lem2  43407  nadd1suc  43424  naddgeoa  43426  oaltom  43437  omltoe  43439  nlimsuc  43473  dfsucon  43555  minregex  43566  onfrALTlem3  44576  onfrALTlem2  44578  onfrALTlem3VD  44918  onfrALTlem2VD  44920  onsetreclem3  49738