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

Theorem 0elon 4931
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 4930 . 2  |-  Ord  (/)
2 0ex 4577 . . 3  |-  (/)  e.  _V
32elon 4887 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 209 1  |-  (/)  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   (/)c0 3785   Ord word 4877   Oncon0 4878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786  df-pw 4012  df-uni 4246  df-tr 4541  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882
This theorem is referenced by:  inton  4935  onn0  4942  on0eqel  4995  orduninsuc  6662  onzsl  6665  smofvon2  7027  tfrlem16  7062  1on  7137  ordgt0ge1  7147  oa0  7166  om0  7167  oe0m  7168  oe0m0  7170  oe0  7172  oesuclem  7175  omcl  7186  oecl  7187  oa0r  7188  om0r  7189  oaord1  7200  oaword1  7201  oaword2  7202  oawordeu  7204  oa00  7208  odi  7228  oeoa  7246  oeoe  7248  nna0r  7258  nnm0r  7259  card2on  7980  card2inf  7981  harcl  7987  cantnfvalf  8084  rankon  8213  cardon  8325  card0  8339  alephon  8450  alephgeom  8463  alephfplem1  8485  cdafi  8570  ttukeylem4  8892  ttukeylem7  8895  cfpwsdom  8959  inar1  9153  rankcf  9155  gruina  9196  rdgprc0  28831  sltval2  29021  sltsolem1  29033  bdayelon  29045  rankeq1o  29433  0hf  29439  onsuccon  29508  onsucsuccmp  29514  harn0  30683  bnj168  32883
  Copyright terms: Public domain W3C validator