Theorem 0elon 6418

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

Syntax hints:   ∈ wcel 2143  ∅c0 4287  Ord word 6361  Oncon0 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-tr 5220  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366

This theorem is referenced by:  inton  6422  onn0  6429  on0eqel  6488  orduninsuc  7840  onzsl  7843  peano1  7886  smofvon2  8344  tfrlem16  8381  rdg0n  8422  1on  8467  ordgt0ge1  8479  oa0  8502  om0  8503  oe0m  8504  oe0m0  8506  oe0  8508  oesuclem  8511  omcl  8522  oecl  8523  oa0r  8524  om0r  8525  oaord1  8537  oaword1  8538  oaword2  8539  oawordeu  8541  oa00  8545  odi  8565  oeoa  8584  oeoe  8586  nna0r  8596  nnm0r  8597  naddrid  8671  naddlid  8672  naddword1  8679  card2on  9517  card2inf  9518  harcl  9522  cantnfvalf  9635  rankon  9768  cardon  9931  card0  9945  alephon  10054  alephgeom  10067  alephfplem1  10089  djufi  10171  cfon  10239  ttukeylem4  10497  ttukeylem7  10500  cfpwsdom  10570  inar1  10761  rankcf  10763  gruina  10804  ltsval2  27798  ltssolem1  27817  nosepnelem  27821  nodense  27834  nolt02o  27837  bdayon  27923  cuteq1  27988  old0  28010  made0  28034  old1  28036  mulsproplem2  28288  mulsproplem3  28289  mulsproplem4  28290  mulsproplem5  28291  mulsproplem6  28292  mulsproplem7  28293  mulsproplem8  28294  mulsproplem12  28298  mulsproplem13  28299  mulsproplem14  28300  precsexlem1  28378  precsexlem2  28379  bnj168  35097  r1wf  35467  fineqvnttrclse  35515  rdgprc0  36261  rankeq1o  36641  0hf  36647  nmulr0  36665  nmull0  36666  nmulss1  36669  onsucconn  36927  onsucsuccmp  36933  finxp1o  38016  finxpreclem4  38018  harn0  43809  onexoegt  43951  ordeldif1o  43967  oe0suclim  43984  oaordnr  44003  nnoeomeqom  44019  oenass  44026  omabs2  44039  omcl3g  44041  naddcnff  44069  nadd2rabex  44093  safesnsupfiss  44121  safesnsupfidom1o  44123  safesnsupfilb  44124  0fno  44141  nlim1NEW  44148  aleph1min  44263  wfaxrep  45683  wfaxnul  45685