Theorem 0elon 6423

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

This proof depends on syntax axioms:   ∈ wcel 2146  ∅c0 4289  Ord word 6366  Oncon0 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-tr 5224  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371

This theorem is used by:  inton  6427  onn0  6434  on0eqel  6493  orduninsuc  7848  onzsl  7851  peano1  7894  smofvon2  8352  tfrlem16  8389  rdg0n  8430  1on  8475  ordgt0ge1  8487  oa0  8510  om0  8511  oe0m  8512  oe0m0  8514  oe0  8516  oesuclem  8519  omcl  8530  oecl  8531  oa0r  8532  om0r  8533  oaord1  8545  oaword1  8546  oaword2  8547  oawordeu  8549  oa00  8553  odi  8573  oeoa  8592  oeoe  8594  nna0r  8604  nnm0r  8605  naddrid  8679  naddlid  8680  naddword1  8687  card2on  9526  card2inf  9527  harcl  9531  cantnfvalf  9644  rankon  9777  cardon  9949  card0  9963  alephon  10072  alephgeom  10085  alephfplem1  10107  djufi  10189  cfon  10256  ttukeylem4  10514  ttukeylem7  10517  cfpwsdom  10587  inar1  10778  rankcf  10780  gruina  10821  ltsval2  27857  ltssolem1  27876  nosepnelem  27880  nodense  27893  nolt02o  27896  bdayon  27982  cuteq1  28047  old0  28069  made0  28093  old1  28095  mulsproplem2  28347  mulsproplem3  28348  mulsproplem4  28349  mulsproplem5  28350  mulsproplem6  28351  mulsproplem7  28352  mulsproplem8  28353  mulsproplem12  28357  mulsproplem13  28358  mulsproplem14  28359  precsexlem1  28437  precsexlem2  28438  bnj168  35151  r1wf  35514  fineqvnttrclse  35561  rdgprc0  36304  rankeq1o  36684  0hf  36690  nmulr0  36708  nmull0  36709  nmulss1  36727  onsucconn  36990  onsucsuccmp  36996  finxp1o  38079  finxpreclem4  38081  harn0  43870  onexoegt  44012  ordeldif1o  44028  oe0suclim  44045  oaordnr  44064  nnoeomeqom  44080  oenass  44087  omabs2  44100  omcl3g  44102  naddcnff  44130  nadd2rabex  44154  safesnsupfiss  44182  safesnsupfidom1o  44184  safesnsupfilb  44185  0fno  44202  nlim1NEW  44209  aleph1min  44324  wfaxrep  45744  wfaxnul  45746