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

Theorem 0elon 4920
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 4919 . 2  |-  Ord  (/)
2 0ex 4569 . . 3  |-  (/)  e.  _V
32elon 4876 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 209 1  |-  (/)  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   (/)c0 3783   Ord word 4866   Oncon0 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3784  df-pw 4001  df-uni 4236  df-tr 4533  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871
This theorem is referenced by:  inton  4924  onn0  4931  on0eqel  4984  orduninsuc  6651  onzsl  6654  smofvon2  7019  tfrlem16  7054  1on  7129  ordgt0ge1  7139  oa0  7158  om0  7159  oe0m  7160  oe0m0  7162  oe0  7164  oesuclem  7167  omcl  7178  oecl  7179  oa0r  7180  om0r  7181  oaord1  7192  oaword1  7193  oaword2  7194  oawordeu  7196  oa00  7200  odi  7220  oeoa  7238  oeoe  7240  nna0r  7250  nnm0r  7251  card2on  7972  card2inf  7973  harcl  7979  cantnfvalf  8075  rankon  8204  cardon  8316  card0  8330  alephon  8441  alephgeom  8454  alephfplem1  8476  cdafi  8561  ttukeylem4  8883  ttukeylem7  8886  cfpwsdom  8950  inar1  9142  rankcf  9144  gruina  9185  rdgprc0  29469  sltval2  29659  sltsolem1  29671  bdayelon  29683  rankeq1o  30059  0hf  30065  onsuccon  30134  onsucsuccmp  30140  harn0  31295  bnj168  34205
  Copyright terms: Public domain W3C validator