Theorem 0elon 6395

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 6394	. 2 ⊢ Ord ∅
2		0ex 5256	. . 3 ⊢ ∅ ∈ V
3	2	elon 6349	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 233	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2141  ∅c0 4285  Ord word 6339  Oncon0 6340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-tr 5207  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6343  df-on 6344

This theorem is referenced by:  inton  6399  onn0  6406  on0eqel  6465  orduninsuc  7817  onzsl  7820  peano1  7863  smofvon2  8320  tfrlem16  8357  rdg0n  8398  1on  8443  ordgt0ge1  8455  oa0  8478  om0  8479  oe0m  8480  oe0m0  8482  oe0  8484  oesuclem  8487  omcl  8498  oecl  8499  oa0r  8500  om0r  8501  oaord1  8513  oaword1  8514  oaword2  8515  oawordeu  8517  oa00  8521  odi  8541  oeoa  8560  oeoe  8562  nna0r  8572  nnm0r  8573  naddrid  8647  naddlid  8648  naddword1  8655  card2on  9497  card2inf  9498  harcl  9502  cantnfvalf  9615  rankon  9748  cardon  9897  card0  9911  alephon  10020  alephgeom  10033  alephfplem1  10055  djufi  10138  cfon  10206  ttukeylem4  10464  ttukeylem7  10467  cfpwsdom  10537  inar1  10728  rankcf  10730  gruina  10771  ltsval2  27695  ltssolem1  27714  nosepnelem  27718  nodense  27731  nolt02o  27734  bdayon  27820  cuteq1  27885  old0  27907  made0  27931  old1  27933  mulsproplem2  28185  mulsproplem3  28186  mulsproplem4  28187  mulsproplem5  28188  mulsproplem6  28189  mulsproplem7  28190  mulsproplem8  28191  mulsproplem12  28195  mulsproplem13  28196  mulsproplem14  28197  precsexlem1  28275  precsexlem2  28276  bnj168  34988  r1wf  35352  fineqvnttrclse  35380  rdgprc0  36094  rankeq1o  36474  0hf  36480  nmulr0  36498  nmull0  36499  onsucconn  36751  onsucsuccmp  36757  finxp1o  37839  finxpreclem4  37841  harn0  43632  onexoegt  43774  ordeldif1o  43790  oe0suclim  43807  oaordnr  43826  nnoeomeqom  43842  oenass  43849  omabs2  43862  omcl3g  43864  naddcnff  43892  nadd2rabex  43916  safesnsupfiss  43944  safesnsupfidom1o  43946  safesnsupfilb  43947  0fno  43964  nlim1NEW  43971  aleph1min  44086  wfaxrep  45523  wfaxnul  45525