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

Theorem 0elon 4854
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

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 4853 . 2
2 0ex 4504 . . 3
32elon 4810 . 2
41, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1757   c0 3719  Ordword 4800   con0 4801
This theorem is referenced by:  inton  4858  onn0  4865  on0eqel  4918  orduninsuc  6538  onzsl  6541  smofvon2  6901  tfrlem16  6936  1on  7011  ordgt0ge1  7021  oa0  7040  om0  7041  oe0m  7042  oe0m0  7044  oe0  7046  oesuclem  7049  omcl  7060  oecl  7061  oa0r  7062  om0r  7063  oaord1  7074  oaword1  7075  oaword2  7076  oawordeu  7078  oa00  7082  odi  7102  oeoa  7120  oeoe  7122  nna0r  7132  nnm0r  7133  card2on  7854  card2inf  7855  harcl  7861  cantnfvalf  7958  rankon  8087  cardon  8199  card0  8213  alephon  8324  alephgeom  8337  alephfplem1  8359  cdafi  8444  ttukeylem4  8766  ttukeylem7  8769  cfpwsdom  8833  inar1  9027  rankcf  9029  gruina  9070  rdgprc0  27725  sltval2  27915  sltsolem1  27927  bdayelon  27939  rankeq1o  28327  0hf  28333  onsuccon  28402  onsucsuccmp  28408  harn0  29580  bnj168  32002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-nul 4503
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-dif 3413  df-in 3417  df-ss 3424  df-nul 3720  df-pw 3944  df-uni 4174  df-tr 4468  df-po 4723  df-so 4724  df-fr 4761  df-we 4763  df-ord 4804  df-on 4805
  Copyright terms: Public domain W3C validator