Theorem 0elon 6380

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

Syntax hints:   ∈ wcel 2114  ∅c0 4287  Ord word 6324  Oncon0 6325

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 5253

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-tr 5208  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329

This theorem is referenced by:  inton  6384  onn0  6391  on0eqel  6450  orduninsuc  7795  onzsl  7798  peano1  7841  smofvon2  8298  tfrlem16  8334  rdg0n  8375  1on  8419  ordgt0ge1  8430  oa0  8453  om0  8454  oe0m  8455  oe0m0  8457  oe0  8459  oesuclem  8462  omcl  8473  oecl  8474  oa0r  8475  om0r  8476  oaord1  8488  oaword1  8489  oaword2  8490  oawordeu  8492  oa00  8496  odi  8516  oeoa  8535  oeoe  8537  nna0r  8547  nnm0r  8548  naddrid  8621  naddlid  8622  naddword1  8629  card2on  9471  card2inf  9472  harcl  9476  cantnfvalf  9586  rankon  9719  cardon  9868  card0  9882  alephon  9991  alephgeom  10004  alephfplem1  10026  djufi  10109  ttukeylem4  10434  ttukeylem7  10437  cfpwsdom  10507  inar1  10698  rankcf  10700  gruina  10741  ltsval2  27636  ltssolem1  27655  nosepnelem  27659  nodense  27672  nolt02o  27675  bdayon  27760  cuteq1  27825  old0  27847  made0  27871  old1  27873  mulsproplem2  28125  mulsproplem3  28126  mulsproplem4  28127  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  precsexlem1  28215  precsexlem2  28216  bnj168  34906  r1wf  35271  fineqvnttrclse  35299  rdgprc0  36004  rankeq1o  36384  0hf  36390  onsucconn  36651  onsucsuccmp  36657  finxp1o  37641  finxpreclem4  37643  harn0  43453  onexoegt  43595  ordeldif1o  43611  oe0suclim  43628  oaordnr  43647  nnoeomeqom  43663  oenass  43670  omabs2  43683  omcl3g  43685  naddcnff  43713  nadd2rabex  43737  safesnsupfiss  43765  safesnsupfidom1o  43767  safesnsupfilb  43768  0fno  43785  nlim1NEW  43792  aleph1min  43907  wfaxrep  45344  wfaxnul  45346