MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eloni Structured version   Visualization version   GIF version

Theorem eloni 5694
Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
eloni (𝐴 ∈ On → Ord 𝐴)

Proof of Theorem eloni
StepHypRef Expression
1 elong 5692 . 2 (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
21ibi 256 1 (𝐴 ∈ On → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Ord word 5683  Oncon0 5684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3188  df-in 3563  df-ss 3570  df-uni 4405  df-tr 4715  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-ord 5687  df-on 5688
This theorem is referenced by:  onelon  5709  onin  5715  ontri1  5718  onfr  5724  onelpss  5725  onsseleq  5726  onelss  5727  ontr1  5732  ontr2  5733  ordunidif  5734  on0eln0  5741  ordsssuc  5773  onsssuc  5774  onnbtwn  5779  suc11  5792  onordi  5793  onssneli  5798  ordon  6932  ordeleqon  6938  onss  6940  ordsuc  6964  onpwsuc  6966  onpsssuc  6969  onsucmin  6971  ordunpr  6976  ordunisuc  6982  onsucuni2  6984  onuninsuci  6990  ordunisuc2  6994  ordzsl  6995  onzsl  6996  nlimon  7001  tfinds  7009  tfindsg2  7011  nnord  7023  onfununi  7386  smo11  7409  smoord  7410  smoword  7411  smogt  7412  tfrlem1  7420  tfrlem9a  7430  tfrlem15  7436  tz7.44-2  7451  tz7.48lem  7484  oe0m1  7549  oaordi  7574  oaord  7575  oacan  7576  oawordri  7578  oalimcl  7588  oaass  7589  omord2  7595  omcan  7597  omwordi  7599  omword1  7601  omword2  7602  om00  7603  omlimcl  7606  omass  7608  omeulem2  7611  omopth2  7612  oen0  7614  oeord  7616  oecan  7617  oewordi  7619  oeworde  7621  oelimcl  7628  oeeulem  7629  oeeui  7630  nnarcl  7644  nnawordi  7649  nnawordex  7665  oaabs2  7673  omabs  7675  omsmo  7682  omxpenlem  8008  infensuc  8085  onomeneq  8097  ordiso  8368  ordtypelem2  8371  hartogslem1  8394  cantnflt  8516  cantnfp1lem3  8524  cantnfp1  8525  oemapso  8526  oemapvali  8528  cantnflem1d  8532  cantnflem1  8533  cantnf  8537  oemapwe  8538  cantnffval2  8539  cnfcom  8544  r111  8585  r1ordg  8588  rankonidlem  8638  bndrank  8651  r1pw  8655  r1pwALT  8656  rankbnd2  8679  tcrank  8694  cardprclem  8752  carduni  8754  cardmin2  8771  infxpenlem  8783  alephdom  8851  alephdom2  8857  cardaleph  8859  iscard3  8863  alephfp  8878  dfac12lem1  8912  dfac12lem2  8913  dfac12lem3  8914  cflim2  9032  cofsmo  9038  cfsmolem  9039  coftr  9042  cfcof  9043  fin67  9164  hsmexlem5  9199  zorn2lem6  9270  ttukeylem3  9280  ttukeylem5  9282  ttukeylem6  9283  ttukeylem7  9284  winainflem  9462  r1limwun  9505  r1wunlim  9506  tsksuc  9531  inar1  9544  gruina  9587  grur1a  9588  grur1  9589  dfrdg2  31423  poseq  31472  soseq  31473  nodmord  31528  noextenddif  31546  nodenselem5  31569  ontgval  32093  ontgsucval  32094  onsuctopon  32096  onintopssconn  32102  onsuct0  32103  sucneqond  32866  onsucuni3  32868  aomclem4  37128  aomclem5  37129  onfrALTlem3  38262  onfrALTlem2  38264  onfrALTlem3VD  38627  onfrALTlem2VD  38629  onsetreclem3  41759
  Copyright terms: Public domain W3C validator