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

Theorem 0elon 4445
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 4444 . 2  |-  Ord  (/)
2 0ex 4152 . . 3  |-  (/)  e.  _V
32elon 4401 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 202 1  |-  (/)  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   (/)c0 3457   Ord word 4391   Oncon0 4392
This theorem is referenced by:  inton  4449  onn0  4456  on0eqel  4510  orduninsuc  4634  onzsl  4637  smofvon2  6369  tfrlem16  6405  1on  6482  ordgt0ge1  6492  oa0  6511  om0  6512  oe0m  6513  oe0m0  6515  oe0  6517  oesuclem  6520  omcl  6531  oecl  6532  oa0r  6533  om0r  6534  oaord1  6545  oaword1  6546  oaword2  6547  oawordeu  6549  oa00  6553  odi  6573  oeoa  6591  oeoe  6593  nna0r  6603  nnm0r  6604  card2on  7264  card2inf  7265  harcl  7271  cantnfvalf  7362  rankon  7463  cardon  7573  card0  7587  alephon  7692  alephgeom  7705  alephfplem1  7727  cdafi  7812  ttukeylem4  8135  ttukeylem7  8138  cfpwsdom  8202  inar1  8393  rankcf  8395  gruina  8436  rdgprc0  23552  sltval2  23711  axsltsolem1  23723  bdayelon  23735  rankeq1o  24209  0hf  24215  onsuccon  24285  onsucsuccmp  24291  harn0  26667  bnj168  28026
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-nul 4151
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458  df-pw 3629  df-uni 3830  df-tr 4116  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396
  Copyright terms: Public domain W3C validator