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

Theorem 0elon 6003
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 6002 . 2 Ord ∅
2 0ex 4997 . . 3 ∅ ∈ V
32elon 5958 . 2 (∅ ∈ On ↔ Ord ∅)
41, 3mpbir 222 1 ∅ ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2157  c0 4127  Ord word 5948  Oncon0 5949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-nul 4996
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-in 3787  df-ss 3794  df-nul 4128  df-pw 4364  df-uni 4642  df-tr 4958  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-ord 5952  df-on 5953
This theorem is referenced by:  inton  6007  onn0  6014  on0eqel  6067  orduninsuc  7282  onzsl  7285  smofvon2  7698  tfrlem16  7734  1on  7812  ordgt0ge1  7823  oa0  7842  om0  7843  oe0m  7844  oe0m0  7846  oe0  7848  oesuclem  7851  omcl  7862  oecl  7863  oa0r  7864  om0r  7865  oaord1  7877  oaword1  7878  oaword2  7879  oawordeu  7881  oa00  7885  odi  7905  oeoa  7923  oeoe  7925  nna0r  7935  nnm0r  7936  card2on  8707  card2inf  8708  harcl  8714  cantnfvalf  8818  rankon  8914  cardon  9062  card0  9076  alephon  9184  alephgeom  9197  alephfplem1  9219  cdafi  9306  ttukeylem4  9628  ttukeylem7  9631  cfpwsdom  9700  inar1  9891  rankcf  9893  gruina  9934  bnj168  31143  rdgprc0  32040  sltval2  32151  sltsolem1  32168  nosepnelem  32172  nodense  32184  nolt02o  32187  bdayelon  32234  rankeq1o  32620  0hf  32626  onsucconn  32775  onsucsuccmp  32781  finxp1o  33563  finxpreclem4  33565  harn0  38190
  Copyright terms: Public domain W3C validator