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

Theorem 0elon 5695
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 ∅ ∈ On

Proof of Theorem 0elon
StepHypRef Expression
1 ord0 5694 . 2 Ord ∅
2 0ex 4718 . . 3 ∅ ∈ V
32elon 5649 . 2 (∅ ∈ On ↔ Ord ∅)
41, 3mpbir 220 1 ∅ ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  c0 3874  Ord word 5639  Oncon0 5640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110  df-uni 4373  df-tr 4681  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644
This theorem is referenced by:  inton  5699  onn0  5706  on0eqel  5762  orduninsuc  6935  onzsl  6938  smofvon2  7340  tfrlem16  7376  1on  7454  ordgt0ge1  7464  oa0  7483  om0  7484  oe0m  7485  oe0m0  7487  oe0  7489  oesuclem  7492  omcl  7503  oecl  7504  oa0r  7505  om0r  7506  oaord1  7518  oaword1  7519  oaword2  7520  oawordeu  7522  oa00  7526  odi  7546  oeoa  7564  oeoe  7566  nna0r  7576  nnm0r  7577  card2on  8342  card2inf  8343  harcl  8349  cantnfvalf  8445  rankon  8541  cardon  8653  card0  8667  alephon  8775  alephgeom  8788  alephfplem1  8810  cdafi  8895  ttukeylem4  9217  ttukeylem7  9220  cfpwsdom  9285  inar1  9476  rankcf  9478  gruina  9519  bnj168  30052  rdgprc0  30943  sltval2  31053  sltsolem1  31067  bdayelon  31079  rankeq1o  31448  0hf  31454  onsuccon  31607  onsucsuccmp  31613  finxp1o  32405  finxpreclem4  32407  harn0  36691
  Copyright terms: Public domain W3C validator