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

Theorem 0elon 5681
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 5680 . 2 Ord ∅
2 0ex 4713 . . 3 ∅ ∈ V
32elon 5635 . 2 (∅ ∈ On ↔ Ord ∅)
41, 3mpbir 219 1 ∅ ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  c0 3873  Ord word 5625  Oncon0 5626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-nul 4712
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-in 3546  df-ss 3553  df-nul 3874  df-pw 4109  df-uni 4367  df-tr 4675  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-ord 5629  df-on 5630
This theorem is referenced by:  inton  5685  onn0  5692  on0eqel  5748  orduninsuc  6912  onzsl  6915  smofvon2  7317  tfrlem16  7353  1on  7431  ordgt0ge1  7441  oa0  7460  om0  7461  oe0m  7462  oe0m0  7464  oe0  7466  oesuclem  7469  omcl  7480  oecl  7481  oa0r  7482  om0r  7483  oaord1  7495  oaword1  7496  oaword2  7497  oawordeu  7499  oa00  7503  odi  7523  oeoa  7541  oeoe  7543  nna0r  7553  nnm0r  7554  card2on  8319  card2inf  8320  harcl  8326  cantnfvalf  8422  rankon  8518  cardon  8630  card0  8644  alephon  8752  alephgeom  8765  alephfplem1  8787  cdafi  8872  ttukeylem4  9194  ttukeylem7  9197  cfpwsdom  9262  inar1  9453  rankcf  9455  gruina  9496  bnj168  29858  rdgprc0  30749  sltval2  30859  sltsolem1  30873  bdayelon  30885  rankeq1o  31254  0hf  31260  onsuccon  31413  onsucsuccmp  31419  finxp1o  32201  finxpreclem4  32203  harn0  36487
  Copyright terms: Public domain W3C validator