Theorem 0elon 6440

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

Syntax hints:   ∈ wcel 2106  ∅c0 4339  Ord word 6385  Oncon0 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-tr 5266  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390

This theorem is referenced by:  inton  6444  onn0  6451  on0eqel  6510  orduninsuc  7864  onzsl  7867  peano1  7911  smofvon2  8395  tfrlem16  8432  rdg0n  8473  1on  8517  1onOLD  8518  ordgt0ge1  8530  oa0  8553  om0  8554  oe0m  8555  oe0m0  8557  oe0  8559  oesuclem  8562  omcl  8573  oecl  8574  oa0r  8575  om0r  8576  oaord1  8588  oaword1  8589  oaword2  8590  oawordeu  8592  oa00  8596  odi  8616  oeoa  8634  oeoe  8636  nna0r  8646  nnm0r  8647  naddrid  8720  naddlid  8721  naddword1  8728  card2on  9592  card2inf  9593  harcl  9597  cantnfvalf  9703  rankon  9833  cardon  9982  card0  9996  alephon  10107  alephgeom  10120  alephfplem1  10142  djufi  10225  ttukeylem4  10550  ttukeylem7  10553  cfpwsdom  10622  inar1  10813  rankcf  10815  gruina  10856  sltval2  27716  sltsolem1  27735  nosepnelem  27739  nodense  27752  nolt02o  27755  bdayelon  27836  cuteq1  27893  old0  27913  made0  27927  old1  27929  mulsproplem2  28158  mulsproplem3  28159  mulsproplem4  28160  mulsproplem5  28161  mulsproplem6  28162  mulsproplem7  28163  mulsproplem8  28164  mulsproplem12  28168  mulsproplem13  28169  mulsproplem14  28170  precsexlem1  28246  precsexlem2  28247  bnj168  34723  rdgprc0  35775  rankeq1o  36153  0hf  36159  onsucconn  36421  onsucsuccmp  36427  finxp1o  37375  finxpreclem4  37377  harn0  43091  onexoegt  43233  ordeldif1o  43250  oe0suclim  43267  oaordnr  43286  nnoeomeqom  43302  oenass  43309  omabs2  43322  omcl3g  43324  naddcnff  43352  nadd2rabex  43376  safesnsupfiss  43405  safesnsupfidom1o  43407  safesnsupfilb  43408  0no  43425  nlim1NEW  43432  aleph1min  43547  wfaxrep  44950