Theorem 0elon 6366

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 6365	. 2 ⊢ Ord ∅
2		0ex 5247	. . 3 ⊢ ∅ ∈ V
3	2	elon 6320	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2113  ∅c0 4282  Ord word 6310  Oncon0 6311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-tr 5201  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6314  df-on 6315

This theorem is referenced by:  inton  6370  onn0  6377  on0eqel  6436  orduninsuc  7779  onzsl  7782  peano1  7825  smofvon2  8282  tfrlem16  8318  rdg0n  8359  1on  8403  ordgt0ge1  8414  oa0  8437  om0  8438  oe0m  8439  oe0m0  8441  oe0  8443  oesuclem  8446  omcl  8457  oecl  8458  oa0r  8459  om0r  8460  oaord1  8472  oaword1  8473  oaword2  8474  oawordeu  8476  oa00  8480  odi  8500  oeoa  8518  oeoe  8520  nna0r  8530  nnm0r  8531  naddrid  8604  naddlid  8605  naddword1  8612  card2on  9447  card2inf  9448  harcl  9452  cantnfvalf  9562  rankon  9695  cardon  9844  card0  9858  alephon  9967  alephgeom  9980  alephfplem1  10002  djufi  10085  ttukeylem4  10410  ttukeylem7  10413  cfpwsdom  10482  inar1  10673  rankcf  10675  gruina  10716  sltval2  27596  sltsolem1  27615  nosepnelem  27619  nodense  27632  nolt02o  27635  bdayelon  27716  cuteq1  27779  old0  27801  made0  27819  old1  27821  mulsproplem2  28057  mulsproplem3  28058  mulsproplem4  28059  mulsproplem5  28060  mulsproplem6  28061  mulsproplem7  28062  mulsproplem8  28063  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  precsexlem1  28146  precsexlem2  28147  bnj168  34763  r1wf  35128  fineqvnttrclse  35165  rdgprc0  35856  rankeq1o  36236  0hf  36242  onsucconn  36503  onsucsuccmp  36509  finxp1o  37457  finxpreclem4  37459  harn0  43220  onexoegt  43362  ordeldif1o  43378  oe0suclim  43395  oaordnr  43414  nnoeomeqom  43430  oenass  43437  omabs2  43450  omcl3g  43452  naddcnff  43480  nadd2rabex  43504  safesnsupfiss  43533  safesnsupfidom1o  43535  safesnsupfilb  43536  0no  43553  nlim1NEW  43560  aleph1min  43675  wfaxrep  45112  wfaxnul  45114