Theorem 0elon 6417

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 6416	. 2 ⊢ Ord ∅
2		0ex 5268	. . 3 ⊢ ∅ ∈ V
3	2	elon 6370	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  ∅c0 4282  Ord word 6360  Oncon0 6361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-tr 5217  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  inton  6421  onn0  6428  on0eqel  6487  orduninsuc  7843  onzsl  7846  peano1  7889  smofvon2  8349  tfrlem16  8386  rdg0n  8427  1on  8472  ordgt0ge1  8484  oa0  8507  om0  8508  oe0m  8509  oe0m0  8511  oe0  8513  oesuclem  8516  omcl  8527  oecl  8528  oa0r  8529  om0r  8530  oaord1  8542  oaword1  8543  oaword2  8544  oawordeu  8546  oa00  8550  odi  8570  oeoa  8589  oeoe  8591  nna0r  8601  nnm0r  8602  naddrid  8676  naddlid  8677  naddword1  8684  card2on  9530  card2inf  9531  harcl  9535  cantnfvalf  9648  rankon  9781  cardon  9953  card0  9967  alephon  10076  alephgeom  10089  alephfplem1  10111  djufi  10193  cfon  10260  ttukeylem4  10518  ttukeylem7  10521  cfpwsdom  10597  inar1  10788  rankcf  10790  gruina  10831  ltsval2  27900  ltssolem1  27919  nosepnelem  27923  nodense  27936  nolt02o  27939  bdayon  28025  cuteq1  28090  old0  28112  made0  28136  old1  28138  mulsproplem2  28390  mulsproplem3  28391  mulsproplem4  28392  mulsproplem5  28393  mulsproplem6  28394  mulsproplem7  28395  mulsproplem8  28396  mulsproplem12  28400  mulsproplem13  28401  mulsproplem14  28402  precsexlem1  28480  precsexlem2  28481  bnj168  35248  r1wf  35611  fineqvnttrclse  35658  rdgprc0  36378  rankeq1o  36759  0hf  36765  nmulr0  36783  nmull0  36784  nmulss1  36802  onsucconn  37065  onsucsuccmp  37071  finxp1o  38154  finxpreclem4  38156  harn0  43951  onexoegt  44093  ordeldif1o  44109  oe0suclim  44126  oaordnr  44145  nnoeomeqom  44161  oenass  44168  omabs2  44181  omcl3g  44183  naddcnff  44211  nadd2rabex  44235  safesnsupfiss  44263  safesnsupfidom1o  44265  safesnsupfilb  44266  0fno  44283  nlim1NEW  44290  aleph1min  44405  wfaxrep  45825  wfaxnul  45827