Theorem 0elon 6372

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

Syntax hints:   ∈ wcel 2114  ∅c0 4274  Ord word 6316  Oncon0 6317

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-tr 5194  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321

This theorem is referenced by:  inton  6376  onn0  6383  on0eqel  6442  orduninsuc  7787  onzsl  7790  peano1  7833  smofvon2  8289  tfrlem16  8325  rdg0n  8366  1on  8410  ordgt0ge1  8421  oa0  8444  om0  8445  oe0m  8446  oe0m0  8448  oe0  8450  oesuclem  8453  omcl  8464  oecl  8465  oa0r  8466  om0r  8467  oaord1  8479  oaword1  8480  oaword2  8481  oawordeu  8483  oa00  8487  odi  8507  oeoa  8526  oeoe  8528  nna0r  8538  nnm0r  8539  naddrid  8612  naddlid  8613  naddword1  8620  card2on  9462  card2inf  9463  harcl  9467  cantnfvalf  9577  rankon  9710  cardon  9859  card0  9873  alephon  9982  alephgeom  9995  alephfplem1  10017  djufi  10100  ttukeylem4  10425  ttukeylem7  10428  cfpwsdom  10498  inar1  10689  rankcf  10691  gruina  10732  ltsval2  27634  ltssolem1  27653  nosepnelem  27657  nodense  27670  nolt02o  27673  bdayon  27758  cuteq1  27823  old0  27845  made0  27869  old1  27871  mulsproplem2  28123  mulsproplem3  28124  mulsproplem4  28125  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  precsexlem1  28213  precsexlem2  28214  bnj168  34889  r1wf  35255  fineqvnttrclse  35284  rdgprc0  35989  rankeq1o  36369  0hf  36375  onsucconn  36636  onsucsuccmp  36642  finxp1o  37722  finxpreclem4  37724  harn0  43548  onexoegt  43690  ordeldif1o  43706  oe0suclim  43723  oaordnr  43742  nnoeomeqom  43758  oenass  43765  omabs2  43778  omcl3g  43780  naddcnff  43808  nadd2rabex  43832  safesnsupfiss  43860  safesnsupfidom1o  43862  safesnsupfilb  43863  0fno  43880  nlim1NEW  43887  aleph1min  44002  wfaxrep  45439  wfaxnul  45441