Theorem 0elon 6436

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

This proof depends on syntax axioms:   ∈ wcel 2147  ∅c0 4281  Ord word 6379  Oncon0 6380

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-tr 5216  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-ord 6383  df-on 6384

This theorem is used by:  inton  6440  onn0  6447  on0eqel  6506  orduninsuc  7878  onzsl  7881  peano1  7924  smofvon2  8392  tfrlem16  8429  rdg0n  8470  1on  8517  ordgt0ge1  8529  oa0  8552  om0  8553  oe0m  8554  oe0m0  8556  oe0  8558  oesuclem  8561  omcl  8572  oecl  8573  oa0r  8574  om0r  8575  oaord1  8587  oaword1  8588  oaword2  8589  oawordeu  8591  oa00  8595  odi  8615  oeoa  8634  oeoe  8636  nna0r  8646  nnm0r  8647  naddrid  8721  naddlid  8722  naddword1  8729  card2on  9575  card2inf  9576  harcl  9580  cantnfvalf  9693  rankon  9830  r1wf  9868  0hf  9944  cardon  10052  card0  10066  alephon  10175  alephgeom  10188  alephfplem1  10210  djufi  10292  cfon  10359  ttukeylem4  10617  ttukeylem7  10620  cfpwsdom  10696  inar1  10887  rankcf  10889  gruina  10930  ltsval2  28043  ltssolem1  28062  nosepnelem  28066  nodense  28079  nolt02o  28082  bdayon  28168  cuteq1  28233  old0  28255  made0  28279  old1  28281  mulsproplem2  28533  mulsproplem3  28534  mulsproplem4  28535  mulsproplem5  28536  mulsproplem6  28537  mulsproplem7  28538  mulsproplem8  28539  mulsproplem12  28543  mulsproplem13  28544  mulsproplem14  28545  precsexlem1  28623  precsexlem2  28624  bnj168  35431  0elscott  35837  acwer1prclem  35851  fineqvnttrclse  35892  j00smo  36005  maxssj0  36006  j0ltalephlem  36007  j0ltaleph  36008  jf1  36010  dfk12  36012  dfk22  36013  dfk32  36014  k1on  36015  k2on  36016  j0le  36019  k3n0j0lt  36020  jltalephlem  36025  jltaleph  36026  rdgprc0  36733  rankeq1o  37110  nmulr0  37122  nmull0  37123  nmulss1  37141  onsucconn  37404  onsucsuccmp  37410  finxp1o  38507  finxpreclem4  38509  harn0  44296  onexoegt  44438  ordeldif1o  44454  oe0suclim  44471  oaordnr  44490  nnoeomeqom  44506  oenass  44513  omabs2  44526  omcl3g  44528  naddcnff  44556  nadd2rabex  44580  safesnsupfiss  44608  safesnsupfidom1o  44610  safesnsupfilb  44611  0fno  44628  nlim1NEW  44635  aleph1min  44750  wfaxrep  46179  wfaxnul  46181