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

Theorem 0elon 4445
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 4444 . 2  |-  Ord  (/)
2 0ex 4150 . . 3  |-  (/)  e.  _V
32elon 4401 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 200 1  |-  (/)  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   (/)c0 3455   Ord word 4391   Oncon0 4392
This theorem is referenced by:  inton  4449  onn0  4456  on0eqel  4510  orduninsuc  4634  onzsl  4637  smofvon2  6373  tfrlem16  6409  1on  6486  ordgt0ge1  6496  oa0  6515  om0  6516  oe0m  6517  oe0m0  6519  oe0  6521  oesuclem  6524  omcl  6535  oecl  6536  oa0r  6537  om0r  6538  oaord1  6549  oaword1  6550  oaword2  6551  oawordeu  6553  oa00  6557  odi  6577  oeoa  6595  oeoe  6597  nna0r  6607  nnm0r  6608  card2on  7268  card2inf  7269  harcl  7275  cantnfvalf  7366  rankon  7467  cardon  7577  card0  7591  alephon  7696  alephgeom  7709  alephfplem1  7731  cdafi  7816  ttukeylem4  8139  ttukeylem7  8142  cfpwsdom  8206  inar1  8397  rankcf  8399  gruina  8440  rdgprc0  24150  sltval2  24310  sltsolem1  24322  bdayelon  24334  rankeq1o  24801  0hf  24807  onsuccon  24877  onsucsuccmp  24883  harn0  27267  bnj168  28758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456  df-pw 3627  df-uni 3828  df-tr 4114  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396
  Copyright terms: Public domain W3C validator