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

Theorem 0elon 4338
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 4337 . 2  |-  Ord  (/)
2 0ex 4047 . . 3  |-  (/)  e.  _V
32elon 4294 . 2  |-  ( (/)  e.  On  <->  Ord  (/) )
41, 3mpbir 202 1  |-  (/)  e.  On
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   (/)c0 3362   Ord word 4284   Oncon0 4285
This theorem is referenced by:  inton  4342  onn0  4349  on0eqel  4401  orduninsuc  4525  onzsl  4528  smofvon2  6259  tfrlem16  6295  1on  6372  ordgt0ge1  6382  oa0  6401  om0  6402  oe0m  6403  oe0m0  6405  oe0  6407  oesuclem  6410  omcl  6421  oecl  6422  oa0r  6423  om0r  6424  oaord1  6435  oaword1  6436  oaword2  6437  oawordeu  6439  oa00  6443  odi  6463  oeoa  6481  oeoe  6483  nna0r  6493  nnm0r  6494  card2on  7152  card2inf  7153  harcl  7159  cantnfvalf  7250  rankon  7351  cardon  7461  card0  7475  alephon  7580  alephgeom  7593  alephfplem1  7615  cdafi  7700  ttukeylem4  8023  ttukeylem7  8026  cfpwsdom  8086  inar1  8277  rankcf  8279  gruina  8320  rdgprc0  23318  sltval2  23477  axsltsolem1  23489  bdayelon  23501  rankeq1o  23975  0hf  23981  onsuccon  24051  onsucsuccmp  24057  harn0  26433  bnj168  27544
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-nul 4046
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363  df-pw 3532  df-uni 3728  df-tr 4011  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289
  Copyright terms: Public domain W3C validator