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

Theorem 0elon 5921
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 5920 . 2 Ord ∅
2 0ex 4921 . . 3 ∅ ∈ V
32elon 5875 . 2 (∅ ∈ On ↔ Ord ∅)
41, 3mpbir 221 1 ∅ ∈ On
Colors of variables: wff setvar class
Syntax hints:  wcel 2144  c0 4061  Ord word 5865  Oncon0 5866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-nul 4920
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735  df-nul 4062  df-pw 4297  df-uni 4573  df-tr 4885  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870
This theorem is referenced by:  inton  5925  onn0  5932  on0eqel  5988  orduninsuc  7189  onzsl  7192  smofvon2  7605  tfrlem16  7641  1on  7719  ordgt0ge1  7730  oa0  7749  om0  7750  oe0m  7751  oe0m0  7753  oe0  7755  oesuclem  7758  omcl  7769  oecl  7770  oa0r  7771  om0r  7772  oaord1  7784  oaword1  7785  oaword2  7786  oawordeu  7788  oa00  7792  odi  7812  oeoa  7830  oeoe  7832  nna0r  7842  nnm0r  7843  card2on  8614  card2inf  8615  harcl  8621  cantnfvalf  8725  rankon  8821  cardon  8969  card0  8983  alephon  9091  alephgeom  9104  alephfplem1  9126  cdafi  9213  ttukeylem4  9535  ttukeylem7  9538  cfpwsdom  9607  inar1  9798  rankcf  9800  gruina  9841  bnj168  31130  rdgprc0  32029  sltval2  32140  sltsolem1  32157  nosepnelem  32161  nodense  32173  nolt02o  32176  bdayelon  32223  rankeq1o  32609  0hf  32615  onsucconn  32768  onsucsuccmp  32774  finxp1o  33559  finxpreclem4  33561  harn0  38191
  Copyright terms: Public domain W3C validator