Theorem eloni 6381

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

Syntax hints:   → wi 4   ∈ wcel 2098  Ord word 6370  Oncon0 6371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3961  df-uni 4910  df-tr 5267  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-ord 6374  df-on 6375

This theorem is referenced by:  onelon  6396  onin  6402  ontri1  6405  onfr  6410  onelpss  6411  onsseleq  6412  onelss  6413  ontr1  6417  ontr2  6418  ordunidif  6420  on0eln0  6427  ordsssuc  6460  onsssuc  6461  onnbtwn  6465  onunel  6476  suc11  6478  onun2  6479  ontr  6480  onordi  6482  onssneli  6487  epweon  7778  epweonALT  7779  ordeleqon  7785  onss  7788  sucexeloni  7813  ordsucOLD  7818  onpwsuc  7820  onpsssuc  7823  onsucmin  7825  ordunpr  7830  ordunisuc  7836  onsucuni2  7838  onuniorsuc  7841  ordunisuc2  7849  ordzsl  7850  onzsl  7851  nlimon  7856  tfinds  7865  tfindsg2  7867  nnord  7879  poseq  8163  soseq  8164  onfununi  8362  smo11  8385  smoord  8386  smoword  8387  smogt  8388  tfrlem1  8397  tfrlem9a  8407  tfrlem15  8413  tz7.44-2  8428  tz7.48lem  8462  ord3  8504  oe0m1  8542  oaordi  8567  oaord  8568  oacan  8569  oawordri  8571  oalimcl  8581  oaass  8582  omord2  8588  omcan  8590  omwordi  8592  omword1  8594  omword2  8595  om00  8596  omlimcl  8599  omass  8601  omeulem2  8604  omopth2  8605  oen0  8607  oeord  8609  oecan  8610  oewordi  8612  oeworde  8614  oelimcl  8621  oeeulem  8622  oeeui  8623  nnarcl  8637  nnawordi  8642  nnawordex  8658  oaabs2  8670  omabs  8672  omsmo  8679  cofonr  8695  naddcllem  8697  omxpenlem  9098  infensuc  9180  dif1enlem  9181  nndomog  9241  nndomogOLD  9251  onomeneq  9253  onomeneqOLD  9254  ordiso  9541  ordtypelem2  9544  hartogslem1  9567  cantnflt  9697  cantnfp1lem3  9705  cantnfp1  9706  oemapso  9707  oemapvali  9709  cantnflem1d  9713  cantnflem1  9714  cantnf  9718  oemapwe  9719  cantnffval2  9720  cnfcom  9725  r111  9800  r1ordg  9803  rankonidlem  9853  bndrank  9866  r1pw  9870  r1pwALT  9871  rankbnd2  9894  tcrank  9909  cardprclem  10004  carduni  10006  cardmin2  10024  infxpenlem  10038  alephdom  10106  alephdom2  10112  cardaleph  10114  iscard3  10118  alephfp  10133  dfac12lem1  10168  dfac12lem2  10169  dfac12lem3  10170  cflim2  10288  cofsmo  10294  cfsmolem  10295  coftr  10298  cfcof  10299  fin67  10420  hsmexlem5  10455  zorn2lem6  10526  ttukeylem3  10536  ttukeylem5  10538  ttukeylem6  10539  ttukeylem7  10540  winainflem  10718  r1limwun  10761  r1wunlim  10762  tsksuc  10787  inar1  10800  gruina  10843  grur1a  10844  grur1  10845  nodmord  27632  noextendseq  27646  noextenddif  27647  nosupno  27682  nosupbday  27684  nosupres  27686  noinfno  27697  noinfbday  27699  noinfres  27701  noetasuplem4  27715  noetainflem4  27719  newbday  27874  dfrdg2  35522  ontgval  36046  ontgsucval  36047  onsuctopon  36049  onintopssconn  36055  onsuct0  36056  sucneqond  36975  onsucuni3  36977  aomclem4  42623  aomclem5  42624  onintunirab  42797  omlimcl2  42812  onelord  42821  oneltri  42828  ordeldifsucon  42830  ordeldif1o  42831  onsucss  42837  onsucf1olem  42841  onov0suclim  42845  oe0rif  42856  onsucwordi  42859  oege1  42877  cantnfresb  42895  omabs2  42903  ordsssucb  42906  tfsconcatlem  42907  tfsconcatfv2  42911  tfsconcatrn  42913  tfsconcatb0  42915  tfsconcat0b  42917  tfsconcatrev  42919  onsucunipr  42943  oaun3lem1  42945  oaun3lem2  42946  nadd1suc  42963  naddsuc2  42964  naddgeoa  42966  oaltom  42977  omltoe  42979  nlimsuc  43013  dfsucon  43095  minregex  43106  onfrALTlem3  44125  onfrALTlem2  44127  onfrALTlem3VD  44468  onfrALTlem2VD  44470  onsetreclem3  48324