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

Theorem eloni 5721
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 5719 . 2 (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
21ibi 256 1 (𝐴 ∈ On → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  Ord word 5710  Oncon0 5711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197  df-in 3574  df-ss 3581  df-uni 4428  df-tr 4744  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-ord 5714  df-on 5715
This theorem is referenced by:  onelon  5736  onin  5742  ontri1  5745  onfr  5751  onelpss  5752  onsseleq  5753  onelss  5754  ontr1  5759  ontr2  5760  ordunidif  5761  on0eln0  5768  ordsssuc  5800  onsssuc  5801  onnbtwn  5806  suc11  5819  onordi  5820  onssneli  5825  ordon  6967  ordeleqon  6973  onss  6975  ordsuc  6999  onpwsuc  7001  onpsssuc  7004  onsucmin  7006  ordunpr  7011  ordunisuc  7017  onsucuni2  7019  onuninsuci  7025  ordunisuc2  7029  ordzsl  7030  onzsl  7031  nlimon  7036  tfinds  7044  tfindsg2  7046  nnord  7058  onfununi  7423  smo11  7446  smoord  7447  smoword  7448  smogt  7449  tfrlem1  7457  tfrlem9a  7467  tfrlem15  7473  tz7.44-2  7488  tz7.48lem  7521  oe0m1  7586  oaordi  7611  oaord  7612  oacan  7613  oawordri  7615  oalimcl  7625  oaass  7626  omord2  7632  omcan  7634  omwordi  7636  omword1  7638  omword2  7639  om00  7640  omlimcl  7643  omass  7645  omeulem2  7648  omopth2  7649  oen0  7651  oeord  7653  oecan  7654  oewordi  7656  oeworde  7658  oelimcl  7665  oeeulem  7666  oeeui  7667  nnarcl  7681  nnawordi  7686  nnawordex  7702  oaabs2  7710  omabs  7712  omsmo  7719  omxpenlem  8046  infensuc  8123  onomeneq  8135  ordiso  8406  ordtypelem2  8409  hartogslem1  8432  cantnflt  8554  cantnfp1lem3  8562  cantnfp1  8563  oemapso  8564  oemapvali  8566  cantnflem1d  8570  cantnflem1  8571  cantnf  8575  oemapwe  8576  cantnffval2  8577  cnfcom  8582  r111  8623  r1ordg  8626  rankonidlem  8676  bndrank  8689  r1pw  8693  r1pwALT  8694  rankbnd2  8717  tcrank  8732  cardprclem  8790  carduni  8792  cardmin2  8809  infxpenlem  8821  alephdom  8889  alephdom2  8895  cardaleph  8897  iscard3  8901  alephfp  8916  dfac12lem1  8950  dfac12lem2  8951  dfac12lem3  8952  cflim2  9070  cofsmo  9076  cfsmolem  9077  coftr  9080  cfcof  9081  fin67  9202  hsmexlem5  9237  zorn2lem6  9308  ttukeylem3  9318  ttukeylem5  9320  ttukeylem6  9321  ttukeylem7  9322  winainflem  9500  r1limwun  9543  r1wunlim  9544  tsksuc  9569  inar1  9582  gruina  9625  grur1a  9626  grur1  9627  dfrdg2  31675  poseq  31724  soseq  31725  nodmord  31780  noextendseq  31794  noextenddif  31795  nosupno  31823  nosupres  31827  noetalem3  31839  ontgval  32405  ontgsucval  32406  onsuctopon  32408  onintopssconn  32414  onsuct0  32415  sucneqond  33184  onsucuni3  33186  aomclem4  37446  aomclem5  37447  onfrALTlem3  38579  onfrALTlem2  38581  onfrALTlem3VD  38943  onfrALTlem2VD  38945  onsetreclem3  42215
  Copyright terms: Public domain W3C validator