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

Theorem 0elon 4936
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

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 4935 . 2
2 0ex 4582 . . 3
32elon 4892 . 2
41, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   c0 3784  Ordword 4882   con0 4883
This theorem is referenced by:  inton  4940  onn0  4947  on0eqel  5000  orduninsuc  6678  onzsl  6681  smofvon2  7046  tfrlem16  7081  1on  7156  ordgt0ge1  7166  oa0  7185  om0  7186  oe0m  7187  oe0m0  7189  oe0  7191  oesuclem  7194  omcl  7205  oecl  7206  oa0r  7207  om0r  7208  oaord1  7219  oaword1  7220  oaword2  7221  oawordeu  7223  oa00  7227  odi  7247  oeoa  7265  oeoe  7267  nna0r  7277  nnm0r  7278  card2on  8001  card2inf  8002  harcl  8008  cantnfvalf  8105  rankon  8234  cardon  8346  card0  8360  alephon  8471  alephgeom  8484  alephfplem1  8506  cdafi  8591  ttukeylem4  8913  ttukeylem7  8916  cfpwsdom  8980  inar1  9174  rankcf  9176  gruina  9217  rdgprc0  29226  sltval2  29416  sltsolem1  29428  bdayelon  29440  rankeq1o  29828  0hf  29834  onsuccon  29903  onsucsuccmp  29909  harn0  31051  bnj168  33785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785  df-pw 4014  df-uni 4250  df-tr 4546  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887
  Copyright terms: Public domain W3C validator