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

Theorem 0elon 4634
Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
0elon  |-  (/)  e.  On

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 4633 . 2  |-  Ord  (/)
2 0ex 4339 . . 3  |-  (/)  e.  _V
32elon 4590 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 201 1  |-  (/)  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   (/)c0 3628   Ord word 4580   Oncon0 4581
This theorem is referenced by:  inton  4638  onn0  4645  on0eqel  4699  orduninsuc  4823  onzsl  4826  smofvon2  6618  tfrlem16  6654  1on  6731  ordgt0ge1  6741  oa0  6760  om0  6761  oe0m  6762  oe0m0  6764  oe0  6766  oesuclem  6769  omcl  6780  oecl  6781  oa0r  6782  om0r  6783  oaord1  6794  oaword1  6795  oaword2  6796  oawordeu  6798  oa00  6802  odi  6822  oeoa  6840  oeoe  6842  nna0r  6852  nnm0r  6853  card2on  7522  card2inf  7523  harcl  7529  cantnfvalf  7620  rankon  7721  cardon  7831  card0  7845  alephon  7950  alephgeom  7963  alephfplem1  7985  cdafi  8070  ttukeylem4  8392  ttukeylem7  8395  cfpwsdom  8459  inar1  8650  rankcf  8652  gruina  8693  rdgprc0  25421  sltval2  25611  sltsolem1  25623  bdayelon  25635  rankeq1o  26112  0hf  26118  onsuccon  26188  onsucsuccmp  26194  harn0  27244  bnj168  29097
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4338
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-in 3327  df-ss 3334  df-nul 3629  df-pw 3801  df-uni 4016  df-tr 4303  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585
  Copyright terms: Public domain W3C validator