Theorem eloni 6393

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Ord word 6382  Oncon0 6383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-ss 3901  df-uni 4871  df-tr 5217  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-ord 6386  df-on 6387

This theorem is used by:  onelon  6408  onin  6415  ontri1  6418  onfr  6423  onelpss  6424  onsseleq  6425  onelss  6426  oneltri  6427  ontr1  6431  ontr2  6432  ordunidif  6434  on0eln0  6441  ordsssuc  6475  onsssuc  6476  onnbtwn  6480  onunel  6491  suc11  6493  onun2  6494  ontr  6495  onordi  6497  onssneli  6501  epweon  7816  epweonALT  7817  ordeleqon  7823  onss  7826  sucexeloni  7850  onpwsuc  7854  onpsssuc  7857  onsucmin  7859  ordunpr  7864  onsucuni2  7872  onuniorsuc  7875  ordunisuc2  7882  ordzsl  7883  onzsl  7884  nlimon  7889  tfinds  7898  tfindsg2  7900  nnord  7912  poseq  8205  soseq  8206  onfununi  8380  smo11  8403  smoord  8404  smoword  8405  smogt  8406  tfrlem1  8414  tfrlem9a  8425  tfrlem15  8431  tz7.44-2  8446  onelfvnef1  8480  tz7.48lemOLD  8482  ord3  8523  oe0m1  8560  oaordi  8585  oaord  8586  oacan  8587  oawordri  8589  oalimcl  8599  oaass  8600  omord2  8606  omcan  8608  omwordi  8610  omword1  8612  omword2  8613  om00  8614  omlimcl  8617  omass  8619  omeulem2  8622  omopth2  8623  oen0  8626  oeord  8628  oecan  8629  oewordi  8631  oeworde  8633  oelimcl  8640  oeeulem  8641  oeeui  8642  nnarcl  8656  nnawordi  8661  nnawordex  8677  oaabs2  8689  omabs  8691  omsmo  8698  cofonr  8714  naddcllem  8716  naddsuc2  8742  omxpenlem  9128  infensuc  9205  dif1enlem  9206  nndomog  9259  onomeneq  9260  ordiso  9540  ordtypelem2  9543  hartogslem1  9566  cantnflt  9703  cantnfp1lem3  9711  cantnfp1  9712  oemapso  9713  oemapvali  9715  cantnflem1d  9719  cantnflem1  9720  cantnf  9724  oemapwe  9725  cantnffval2  9726  cnfcom  9731  r111  9812  r1ordg  9815  rankonidlem  9868  bndrank  9884  r1pw  9889  r1pwALT  9890  rankbnd2  9916  tcrank  9931  cardprclem  10090  carduni  10092  cardmin2  10110  infxpenlem  10122  alephdom  10190  alephdom2  10196  cardaleph  10198  iscard3  10202  alephfp  10217  dfac12lem1  10252  dfac12lem2  10253  dfac12lem3  10254  cflim2  10371  cofsmo  10377  cfsmolem  10378  coftr  10381  cfcof  10382  fin67  10503  hsmexlem5  10538  zorn2lem6  10609  ttukeylem3  10619  ttukeylem5  10621  ttukeylem6  10622  ttukeylem7  10623  winainflem  10808  r1limwun  10851  r1wunlim  10852  tsksuc  10877  inar1  10890  gruina  10933  grur1a  10934  grur1  10935  nodmord  28043  noextendseq  28057  noextenddif  28058  nosupno  28093  nosupbday  28095  nosupres  28097  noinfno  28108  noinfbday  28110  noinfres  28112  noetasuplem4  28126  noetainflem4  28130  newbday  28321  oldfib  28796  fineqvnttrclse  35905  maxssj0  36019  dfrdg2  36748  nmulprop  37130  ontgval  37410  ontgsucval  37411  onsuctopon  37413  onintopssconn  37419  onsuct0  37420  sucneqond  38493  onsucuni3  38495  aomclem4  44263  aomclem5  44264  onintunirab  44432  omlimcl2  44447  onelord  44456  ordeldifsucon  44464  ordeldif1o  44465  onsucss  44471  onsucf1olem  44475  onov0suclim  44479  oe0rif  44490  onsucwordi  44493  oege1  44511  cantnfresb  44529  omabs2  44537  ordsssucb  44540  tfsconcatlem  44541  tfsconcatfv2  44545  tfsconcatrn  44547  tfsconcatb0  44549  tfsconcat0b  44551  tfsconcatrev  44553  onsucunipr  44577  oaun3lem1  44579  oaun3lem2  44580  nadd1suc  44597  naddgeoa  44599  oaltom  44609  omltoe  44611  nlimsuc  44645  dfsucon  44727  minregex  44738  onfrALTlem3  45729  onfrALTlem2  45731  onfrALTlem3VD  46071  onfrALTlem2VD  46073  onsetreclem3  51090