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

This proof depends on syntax axioms:   ∈ wcel 2144  ∅c0 4278  Ord word 6361  Oncon0 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366

This theorem is used by:  inton  6422  onn0  6429  on0eqel  6488  orduninsuc  7854  onzsl  7857  peano1  7900  smofvon2  8367  tfrlem16  8404  rdg0n  8445  1on  8492  ordgt0ge1  8504  oa0  8527  om0  8528  oe0m  8529  oe0m0  8531  oe0  8533  oesuclem  8536  omcl  8547  oecl  8548  oa0r  8549  om0r  8550  oaord1  8562  oaword1  8563  oaword2  8564  oawordeu  8566  oa00  8570  odi  8590  oeoa  8609  oeoe  8611  nna0r  8621  nnm0r  8622  naddrid  8696  naddlid  8697  naddword1  8704  card2on  9551  card2inf  9552  harcl  9556  cantnfvalf  9669  rankon  9806  r1wf  9844  0hf  9920  cardon  10028  card0  10042  alephon  10151  alephgeom  10164  alephfplem1  10186  djufi  10268  cfon  10335  ttukeylem4  10593  ttukeylem7  10596  cfpwsdom  10672  inar1  10863  rankcf  10865  gruina  10906  ltsval2  28018  ltssolem1  28037  nosepnelem  28041  nodense  28054  nolt02o  28057  bdayon  28143  cuteq1  28208  old0  28230  made0  28254  old1  28256  mulsproplem2  28508  mulsproplem3  28509  mulsproplem4  28510  mulsproplem5  28511  mulsproplem6  28512  mulsproplem7  28513  mulsproplem8  28514  mulsproplem12  28518  mulsproplem13  28519  mulsproplem14  28520  precsexlem1  28598  precsexlem2  28599  bnj168  35407  acwer1prclem  35815  fineqvnttrclse  35848  j00smo  35944  maxssj0  35945  j0ltalephlem  35946  j0ltaleph  35947  rdgprc0  36647  rankeq1o  37024  nmulr0  37036  nmull0  37037  nmulss1  37055  onsucconn  37318  onsucsuccmp  37324  finxp1o  38408  finxpreclem4  38410  harn0  44197  onexoegt  44339  ordeldif1o  44355  oe0suclim  44372  oaordnr  44391  nnoeomeqom  44407  oenass  44414  omabs2  44427  omcl3g  44429  naddcnff  44457  nadd2rabex  44481  safesnsupfiss  44509  safesnsupfidom1o  44511  safesnsupfilb  44512  0fno  44529  nlim1NEW  44536  aleph1min  44651  wfaxrep  46077  wfaxnul  46079