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

Theorem 0elon 5747
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 5746 . 2 Ord ∅
2 0ex 4760 . . 3 ∅ ∈ V
32elon 5701 . 2 (∅ ∈ On ↔ Ord ∅)
41, 3mpbir 221 1 ∅ ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  c0 3897  Ord word 5691  Oncon0 5692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-in 3567  df-ss 3574  df-nul 3898  df-pw 4138  df-uni 4410  df-tr 4723  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696
This theorem is referenced by:  inton  5751  onn0  5758  on0eqel  5814  orduninsuc  7005  onzsl  7008  smofvon2  7413  tfrlem16  7449  1on  7527  ordgt0ge1  7537  oa0  7556  om0  7557  oe0m  7558  oe0m0  7560  oe0  7562  oesuclem  7565  omcl  7576  oecl  7577  oa0r  7578  om0r  7579  oaord1  7591  oaword1  7592  oaword2  7593  oawordeu  7595  oa00  7599  odi  7619  oeoa  7637  oeoe  7639  nna0r  7649  nnm0r  7650  card2on  8419  card2inf  8420  harcl  8426  cantnfvalf  8522  rankon  8618  cardon  8730  card0  8744  alephon  8852  alephgeom  8865  alephfplem1  8887  cdafi  8972  ttukeylem4  9294  ttukeylem7  9297  cfpwsdom  9366  inar1  9557  rankcf  9559  gruina  9600  bnj168  30559  rdgprc0  31453  sltval2  31563  sltsolem1  31581  bdayelon  31596  nosepnelem  31618  rankeq1o  31973  0hf  31979  onsucconn  32132  onsucsuccmp  32138  finxp1o  32900  finxpreclem4  32902  harn0  37192
  Copyright terms: Public domain W3C validator