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

Theorem 0elon 5483
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 5482 . 2  |-  Ord  (/)
2 0ex 4528 . . 3  |-  (/)  e.  _V
32elon 5439 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 214 1  |-  (/)  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1904   (/)c0 3722   Ord word 5429   Oncon0 5430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-nul 4527
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-in 3397  df-ss 3404  df-nul 3723  df-pw 3944  df-uni 4191  df-tr 4491  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-ord 5433  df-on 5434
This theorem is referenced by:  inton  5487  onn0  5494  on0eqel  5547  orduninsuc  6689  onzsl  6692  smofvon2  7093  tfrlem16  7129  1on  7207  ordgt0ge1  7217  oa0  7236  om0  7237  oe0m  7238  oe0m0  7240  oe0  7242  oesuclem  7245  omcl  7256  oecl  7257  oa0r  7258  om0r  7259  oaord1  7270  oaword1  7271  oaword2  7272  oawordeu  7274  oa00  7278  odi  7298  oeoa  7316  oeoe  7318  nna0r  7328  nnm0r  7329  card2on  8087  card2inf  8088  harcl  8094  cantnfvalf  8188  rankon  8284  cardon  8396  card0  8410  alephon  8518  alephgeom  8531  alephfplem1  8553  cdafi  8638  ttukeylem4  8960  ttukeylem7  8963  cfpwsdom  9027  inar1  9218  rankcf  9220  gruina  9261  bnj168  29610  rdgprc0  30511  sltval2  30614  sltsolem1  30628  bdayelon  30640  rankeq1o  31009  0hf  31015  onsuccon  31169  onsucsuccmp  31175  finxp1o  31854  finxpreclem4  31856  harn0  36032
  Copyright terms: Public domain W3C validator