Theorem 0elon 6378

Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 17-Sep-1993.)

Assertion

Ref	Expression
0elon	⊢ ∅ ∈ On

Proof of Theorem 0elon

Step	Hyp	Ref	Expression
1		ord0 6377	. 2 ⊢ Ord ∅
2		0ex 5242	. . 3 ⊢ ∅ ∈ V
3	2	elon 6332	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2114  ∅c0 4273  Ord word 6322  Oncon0 6323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-tr 5193  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327

This theorem is referenced by:  inton  6382  onn0  6389  on0eqel  6448  orduninsuc  7794  onzsl  7797  peano1  7840  smofvon2  8296  tfrlem16  8332  rdg0n  8373  1on  8417  ordgt0ge1  8428  oa0  8451  om0  8452  oe0m  8453  oe0m0  8455  oe0  8457  oesuclem  8460  omcl  8471  oecl  8472  oa0r  8473  om0r  8474  oaord1  8486  oaword1  8487  oaword2  8488  oawordeu  8490  oa00  8494  odi  8514  oeoa  8533  oeoe  8535  nna0r  8545  nnm0r  8546  naddrid  8619  naddlid  8620  naddword1  8627  card2on  9469  card2inf  9470  harcl  9474  cantnfvalf  9586  rankon  9719  cardon  9868  card0  9882  alephon  9991  alephgeom  10004  alephfplem1  10026  djufi  10109  ttukeylem4  10434  ttukeylem7  10437  cfpwsdom  10507  inar1  10698  rankcf  10700  gruina  10741  ltsval2  27620  ltssolem1  27639  nosepnelem  27643  nodense  27656  nolt02o  27659  bdayon  27744  cuteq1  27809  old0  27831  made0  27855  old1  27857  mulsproplem2  28109  mulsproplem3  28110  mulsproplem4  28111  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  precsexlem1  28199  precsexlem2  28200  bnj168  34873  r1wf  35239  fineqvnttrclse  35268  rdgprc0  35973  rankeq1o  36353  0hf  36359  onsucconn  36620  onsucsuccmp  36626  finxp1o  37708  finxpreclem4  37710  harn0  43530  onexoegt  43672  ordeldif1o  43688  oe0suclim  43705  oaordnr  43724  nnoeomeqom  43740  oenass  43747  omabs2  43760  omcl3g  43762  naddcnff  43790  nadd2rabex  43814  safesnsupfiss  43842  safesnsupfidom1o  43844  safesnsupfilb  43845  0fno  43862  nlim1NEW  43869  aleph1min  43984  wfaxrep  45421  wfaxnul  45423