Theorem 0elon 6438

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

Syntax hints:   ∈ wcel 2108  ∅c0 4333  Ord word 6383  Oncon0 6384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388

This theorem is referenced by:  inton  6442  onn0  6449  on0eqel  6508  orduninsuc  7864  onzsl  7867  peano1  7910  smofvon2  8396  tfrlem16  8433  rdg0n  8474  1on  8518  1onOLD  8519  ordgt0ge1  8531  oa0  8554  om0  8555  oe0m  8556  oe0m0  8558  oe0  8560  oesuclem  8563  omcl  8574  oecl  8575  oa0r  8576  om0r  8577  oaord1  8589  oaword1  8590  oaword2  8591  oawordeu  8593  oa00  8597  odi  8617  oeoa  8635  oeoe  8637  nna0r  8647  nnm0r  8648  naddrid  8721  naddlid  8722  naddword1  8729  card2on  9594  card2inf  9595  harcl  9599  cantnfvalf  9705  rankon  9835  cardon  9984  card0  9998  alephon  10109  alephgeom  10122  alephfplem1  10144  djufi  10227  ttukeylem4  10552  ttukeylem7  10555  cfpwsdom  10624  inar1  10815  rankcf  10817  gruina  10858  sltval2  27701  sltsolem1  27720  nosepnelem  27724  nodense  27737  nolt02o  27740  bdayelon  27821  cuteq1  27878  old0  27898  made0  27912  old1  27914  mulsproplem2  28143  mulsproplem3  28144  mulsproplem4  28145  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  precsexlem1  28231  precsexlem2  28232  bnj168  34744  rdgprc0  35794  rankeq1o  36172  0hf  36178  onsucconn  36439  onsucsuccmp  36445  finxp1o  37393  finxpreclem4  37395  harn0  43114  onexoegt  43256  ordeldif1o  43273  oe0suclim  43290  oaordnr  43309  nnoeomeqom  43325  oenass  43332  omabs2  43345  omcl3g  43347  naddcnff  43375  nadd2rabex  43399  safesnsupfiss  43428  safesnsupfidom1o  43430  safesnsupfilb  43431  0no  43448  nlim1NEW  43455  aleph1min  43570  wfaxrep  45011  wfaxnul  45013