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

Theorem 0elon 4417
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 4416 . 2  |-  Ord  (/)
2 0ex 4124 . . 3  |-  (/)  e.  _V
32elon 4373 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 202 1  |-  (/)  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   (/)c0 3430   Ord word 4363   Oncon0 4364
This theorem is referenced by:  inton  4421  onn0  4428  on0eqel  4482  orduninsuc  4606  onzsl  4609  smofvon2  6341  tfrlem16  6377  1on  6454  ordgt0ge1  6464  oa0  6483  om0  6484  oe0m  6485  oe0m0  6487  oe0  6489  oesuclem  6492  omcl  6503  oecl  6504  oa0r  6505  om0r  6506  oaord1  6517  oaword1  6518  oaword2  6519  oawordeu  6521  oa00  6525  odi  6545  oeoa  6563  oeoe  6565  nna0r  6575  nnm0r  6576  card2on  7236  card2inf  7237  harcl  7243  cantnfvalf  7334  rankon  7435  cardon  7545  card0  7559  alephon  7664  alephgeom  7677  alephfplem1  7699  cdafi  7784  ttukeylem4  8107  ttukeylem7  8110  cfpwsdom  8174  inar1  8365  rankcf  8367  gruina  8408  rdgprc0  23519  sltval2  23678  axsltsolem1  23690  bdayelon  23702  rankeq1o  24176  0hf  24182  onsuccon  24252  onsucsuccmp  24258  harn0  26634  bnj168  27807
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 2239  ax-nul 4123
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431  df-pw 3601  df-uni 3802  df-tr 4088  df-po 4286  df-so 4287  df-fr 4324  df-we 4326  df-ord 4367  df-on 4368
  Copyright terms: Public domain W3C validator