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

Theorem 0elon 4921
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 4920 . 2  |-  Ord  (/)
2 0ex 4567 . . 3  |-  (/)  e.  _V
32elon 4877 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 209 1  |-  (/)  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   (/)c0 3770   Ord word 4867   Oncon0 4868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-nul 4566
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3771  df-pw 3999  df-uni 4235  df-tr 4531  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872
This theorem is referenced by:  inton  4925  onn0  4932  on0eqel  4985  orduninsuc  6663  onzsl  6666  smofvon2  7029  tfrlem16  7064  1on  7139  ordgt0ge1  7149  oa0  7168  om0  7169  oe0m  7170  oe0m0  7172  oe0  7174  oesuclem  7177  omcl  7188  oecl  7189  oa0r  7190  om0r  7191  oaord1  7202  oaword1  7203  oaword2  7204  oawordeu  7206  oa00  7210  odi  7230  oeoa  7248  oeoe  7250  nna0r  7260  nnm0r  7261  card2on  7983  card2inf  7984  harcl  7990  cantnfvalf  8087  rankon  8216  cardon  8328  card0  8342  alephon  8453  alephgeom  8466  alephfplem1  8488  cdafi  8573  ttukeylem4  8895  ttukeylem7  8898  cfpwsdom  8962  inar1  9156  rankcf  9158  gruina  9199  rdgprc0  29202  sltval2  29392  sltsolem1  29404  bdayelon  29416  rankeq1o  29804  0hf  29810  onsuccon  29879  onsucsuccmp  29885  harn0  31027  bnj168  33653
  Copyright terms: Public domain W3C validator