Theorem 0elon 6405

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 6404	. 2 ⊢ Ord ∅
2		0ex 5262	. . 3 ⊢ ∅ ∈ V
3	2	elon 6359	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2145  ∅c0 4288  Ord word 6349  Oncon0 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-tr 5213  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-ord 6353  df-on 6354

This theorem is referenced by:  inton  6409  onn0  6416  on0eqel  6475  orduninsuc  7827  onzsl  7830  peano1  7873  smofvon2  8331  tfrlem16  8368  rdg0n  8409  1on  8454  ordgt0ge1  8466  oa0  8489  om0  8490  oe0m  8491  oe0m0  8493  oe0  8495  oesuclem  8498  omcl  8509  oecl  8510  oa0r  8511  om0r  8512  oaord1  8524  oaword1  8525  oaword2  8526  oawordeu  8528  oa00  8532  odi  8552  oeoa  8571  oeoe  8573  nna0r  8583  nnm0r  8584  naddrid  8658  naddlid  8659  naddword1  8666  card2on  9504  card2inf  9505  harcl  9509  cantnfvalf  9622  rankon  9755  cardon  9918  card0  9932  alephon  10041  alephgeom  10054  alephfplem1  10076  djufi  10158  cfon  10226  ttukeylem4  10484  ttukeylem7  10487  cfpwsdom  10557  inar1  10748  rankcf  10750  gruina  10791  ltsval2  27778  ltssolem1  27797  nosepnelem  27801  nodense  27814  nolt02o  27817  bdayon  27903  cuteq1  27968  old0  27990  made0  28014  old1  28016  mulsproplem2  28268  mulsproplem3  28269  mulsproplem4  28270  mulsproplem5  28271  mulsproplem6  28272  mulsproplem7  28273  mulsproplem8  28274  mulsproplem12  28278  mulsproplem13  28279  mulsproplem14  28280  precsexlem1  28358  precsexlem2  28359  bnj168  35036  r1wf  35404  fineqvnttrclse  35432  rdgprc0  36154  rankeq1o  36534  0hf  36540  nmulr0  36558  nmull0  36559  onsucconn  36811  onsucsuccmp  36817  finxp1o  37898  finxpreclem4  37900  harn0  43691  onexoegt  43833  ordeldif1o  43849  oe0suclim  43866  oaordnr  43885  nnoeomeqom  43901  oenass  43908  omabs2  43921  omcl3g  43923  naddcnff  43951  nadd2rabex  43975  safesnsupfiss  44003  safesnsupfidom1o  44005  safesnsupfilb  44006  0fno  44023  nlim1NEW  44030  aleph1min  44145  wfaxrep  45568  wfaxnul  45570