Theorem 0elon 6419

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 6418	. 2 ⊢ Ord ∅
2		0ex 5308	. . 3 ⊢ ∅ ∈ V
3	2	elon 6374	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 230	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2107  ∅c0 4323  Ord word 6364  Oncon0 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369

This theorem is referenced by:  inton  6423  onn0  6430  on0eqel  6489  orduninsuc  7832  onzsl  7835  peano1  7879  smofvon2  8356  tfrlem16  8393  rdg0n  8434  1on  8478  1onOLD  8479  ordgt0ge1  8493  oa0  8516  om0  8517  oe0m  8518  oe0m0  8520  oe0  8522  oesuclem  8525  omcl  8536  oecl  8537  oa0r  8538  om0r  8539  oaord1  8551  oaword1  8552  oaword2  8553  oawordeu  8555  oa00  8559  odi  8579  oeoa  8597  oeoe  8599  nna0r  8609  nnm0r  8610  naddrid  8682  naddlid  8683  naddword1  8690  card2on  9549  card2inf  9550  harcl  9554  cantnfvalf  9660  rankon  9790  cardon  9939  card0  9953  alephon  10064  alephgeom  10077  alephfplem1  10099  djufi  10181  ttukeylem4  10507  ttukeylem7  10510  cfpwsdom  10579  inar1  10770  rankcf  10772  gruina  10813  sltval2  27159  sltsolem1  27178  nosepnelem  27182  nodense  27195  nolt02o  27198  bdayelon  27278  cuteq1  27334  old0  27354  made0  27368  old1  27370  mulsproplem2  27573  mulsproplem3  27574  mulsproplem4  27575  mulsproplem5  27576  mulsproplem6  27577  mulsproplem7  27578  mulsproplem8  27579  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  precsexlem1  27653  precsexlem2  27654  bnj168  33741  rdgprc0  34765  rankeq1o  35143  0hf  35149  onsucconn  35323  onsucsuccmp  35329  finxp1o  36273  finxpreclem4  36275  harn0  41844  onexoegt  41993  ordeldif1o  42010  oe0suclim  42027  oaordnr  42046  nnoeomeqom  42062  oenass  42069  omabs2  42082  omcl3g  42084  naddcnff  42112  nadd2rabex  42136  safesnsupfiss  42166  safesnsupfidom1o  42168  safesnsupfilb  42169  0no  42186  nlim1NEW  42193  aleph1min  42308