Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elon Unicode version

Theorem elon 4545
 Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
Hypothesis
Ref Expression
elon.1
Assertion
Ref Expression
elon

Proof of Theorem elon
StepHypRef Expression
1 elon.1 . 2
2 elong 4544 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wb 177   wcel 1721  cvv 2913   word 4535  con0 4536 This theorem is referenced by:  tron  4559  0elon  4589  smogt  6579  rdglim2  6640  omeulem1  6775  isfinite2  7315  r0weon  7841  cflim3  8089  inar1  8597  tfrALTlem  25459  ellimits  25633  limitssson  25634  dford3lem2  26950 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ral 2668  df-rex 2669  df-v 2915  df-in 3284  df-ss 3291  df-uni 3972  df-tr 4258  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540
 Copyright terms: Public domain W3C validator