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

Theorem 0elon 6368
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 ∅ ∈ On

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 6367 . 2 Ord ∅
2 0ex 5263 . . 3 ∅ ∈ V
32elon 6323 . 2 (∅ ∈ On ↔ Ord ∅)
41, 3mpbir 230 1 ∅ ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  c0 4281  Ord word 6313  Oncon0 6314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-nul 5262
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-tr 5222  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-ord 6317  df-on 6318
This theorem is referenced by:  inton  6372  onn0  6379  on0eqel  6437  orduninsuc  7770  onzsl  7773  peano1  7816  smofvon2  8270  tfrlem16  8307  rdg0n  8348  1on  8392  1onOLD  8393  ordgt0ge1  8407  oa0  8430  om0  8431  oe0m  8432  oe0m0  8434  oe0  8436  oesuclem  8439  omcl  8450  oecl  8451  oa0r  8452  om0r  8453  oaord1  8466  oaword1  8467  oaword2  8468  oawordeu  8470  oa00  8474  odi  8494  oeoa  8512  oeoe  8514  nna0r  8524  nnm0r  8525  card2on  9424  card2inf  9425  harcl  9429  cantnfvalf  9535  rankon  9665  cardon  9814  card0  9828  alephon  9939  alephgeom  9952  alephfplem1  9974  djufi  10056  ttukeylem4  10382  ttukeylem7  10385  cfpwsdom  10454  inar1  10645  rankcf  10647  gruina  10688  sltval2  26932  sltsolem1  26951  nosepnelem  26955  nodense  26968  nolt02o  26971  bdayelon  27044  old0  27117  made0  27131  bnj168  33122  rdgprc0  34162  naddid1  34232  naddword1  34239  rankeq1o  34687  0hf  34693  onsucconn  34841  onsucsuccmp  34847  finxp1o  35794  finxpreclem4  35796  harn0  41331  omabs2  41459  omcl3g  41461  naddcnff  41470  safesnsupfiss  41486  safesnsupfidom1o  41488  safesnsupfilb  41489  0no  41506  nlim1NEW  41513  aleph1min  41628
  Copyright terms: Public domain W3C validator