Theorem 0elon 6361

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 6360	. 2 ⊢ Ord ∅
2		0ex 5245	. . 3 ⊢ ∅ ∈ V
3	2	elon 6315	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2111  ∅c0 4283  Ord word 6305  Oncon0 6306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-tr 5199  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-ord 6309  df-on 6310

This theorem is referenced by:  inton  6365  onn0  6372  on0eqel  6431  orduninsuc  7773  onzsl  7776  peano1  7819  smofvon2  8276  tfrlem16  8312  rdg0n  8353  1on  8397  ordgt0ge1  8408  oa0  8431  om0  8432  oe0m  8433  oe0m0  8435  oe0  8437  oesuclem  8440  omcl  8451  oecl  8452  oa0r  8453  om0r  8454  oaord1  8466  oaword1  8467  oaword2  8468  oawordeu  8470  oa00  8474  odi  8494  oeoa  8512  oeoe  8514  nna0r  8524  nnm0r  8525  naddrid  8598  naddlid  8599  naddword1  8606  card2on  9440  card2inf  9441  harcl  9445  cantnfvalf  9555  rankon  9688  cardon  9837  card0  9851  alephon  9960  alephgeom  9973  alephfplem1  9995  djufi  10078  ttukeylem4  10403  ttukeylem7  10406  cfpwsdom  10475  inar1  10666  rankcf  10668  gruina  10709  sltval2  27596  sltsolem1  27615  nosepnelem  27619  nodense  27632  nolt02o  27635  bdayelon  27716  cuteq1  27779  old0  27801  made0  27819  old1  27821  mulsproplem2  28057  mulsproplem3  28058  mulsproplem4  28059  mulsproplem5  28060  mulsproplem6  28061  mulsproplem7  28062  mulsproplem8  28063  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  precsexlem1  28146  precsexlem2  28147  bnj168  34740  r1wf  35105  fineqvnttrclse  35142  rdgprc0  35833  rankeq1o  36211  0hf  36217  onsucconn  36478  onsucsuccmp  36484  finxp1o  37432  finxpreclem4  37434  harn0  43141  onexoegt  43283  ordeldif1o  43299  oe0suclim  43316  oaordnr  43335  nnoeomeqom  43351  oenass  43358  omabs2  43371  omcl3g  43373  naddcnff  43401  nadd2rabex  43425  safesnsupfiss  43454  safesnsupfidom1o  43456  safesnsupfilb  43457  0no  43474  nlim1NEW  43481  aleph1min  43596  wfaxrep  45033  wfaxnul  45035