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

Theorem 0elon 4382
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 4381 . 2  |-  Ord  (/)
2 0ex 4090 . . 3  |-  (/)  e.  _V
32elon 4338 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 202 1  |-  (/)  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   (/)c0 3397   Ord word 4328   Oncon0 4329
This theorem is referenced by:  inton  4386  onn0  4393  on0eqel  4447  orduninsuc  4571  onzsl  4574  smofvon2  6306  tfrlem16  6342  1on  6419  ordgt0ge1  6429  oa0  6448  om0  6449  oe0m  6450  oe0m0  6452  oe0  6454  oesuclem  6457  omcl  6468  oecl  6469  oa0r  6470  om0r  6471  oaord1  6482  oaword1  6483  oaword2  6484  oawordeu  6486  oa00  6490  odi  6510  oeoa  6528  oeoe  6530  nna0r  6540  nnm0r  6541  card2on  7201  card2inf  7202  harcl  7208  cantnfvalf  7299  rankon  7400  cardon  7510  card0  7524  alephon  7629  alephgeom  7642  alephfplem1  7664  cdafi  7749  ttukeylem4  8072  ttukeylem7  8075  cfpwsdom  8139  inar1  8330  rankcf  8332  gruina  8373  rdgprc0  23484  sltval2  23643  axsltsolem1  23655  bdayelon  23667  rankeq1o  24141  0hf  24147  onsuccon  24217  onsucsuccmp  24223  harn0  26599  bnj168  27770
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-nul 4089
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398  df-pw 3568  df-uni 3769  df-tr 4054  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333
  Copyright terms: Public domain W3C validator