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

Theorem 0elon 4784
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  |-  (/)  e.  On

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 4783 . 2  |-  Ord  (/)
2 0ex 4434 . . 3  |-  (/)  e.  _V
32elon 4740 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 209 1  |-  (/)  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   (/)c0 3649   Ord word 4730   Oncon0 4731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4433
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-in 3347  df-ss 3354  df-nul 3650  df-pw 3874  df-uni 4104  df-tr 4398  df-po 4653  df-so 4654  df-fr 4691  df-we 4693  df-ord 4734  df-on 4735
This theorem is referenced by:  inton  4788  onn0  4795  on0eqel  4848  orduninsuc  6466  onzsl  6469  smofvon2  6829  tfrlem16  6864  1on  6939  ordgt0ge1  6949  oa0  6968  om0  6969  oe0m  6970  oe0m0  6972  oe0  6974  oesuclem  6977  omcl  6988  oecl  6989  oa0r  6990  om0r  6991  oaord1  7002  oaword1  7003  oaword2  7004  oawordeu  7006  oa00  7010  odi  7030  oeoa  7048  oeoe  7050  nna0r  7060  nnm0r  7061  card2on  7781  card2inf  7782  harcl  7788  cantnfvalf  7885  rankon  8014  cardon  8126  card0  8140  alephon  8251  alephgeom  8264  alephfplem1  8286  cdafi  8371  ttukeylem4  8693  ttukeylem7  8696  cfpwsdom  8760  inar1  8954  rankcf  8956  gruina  8997  rdgprc0  27619  sltval2  27809  sltsolem1  27821  bdayelon  27833  rankeq1o  28221  0hf  28227  onsuccon  28296  onsucsuccmp  28302  harn0  29470  bnj168  31733
  Copyright terms: Public domain W3C validator