Theorem 0elon 6397

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 6396	. 2 ⊢ Ord ∅
2		0ex 5256	. . 3 ⊢ ∅ ∈ V
3	2	elon 6351	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 233	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2141  ∅c0 4285  Ord word 6341  Oncon0 6342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-tr 5207  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346

This theorem is referenced by:  inton  6401  onn0  6408  on0eqel  6467  orduninsuc  7819  onzsl  7822  peano1  7865  smofvon2  8322  tfrlem16  8359  rdg0n  8400  1on  8445  ordgt0ge1  8457  oa0  8480  om0  8481  oe0m  8482  oe0m0  8484  oe0  8486  oesuclem  8489  omcl  8500  oecl  8501  oa0r  8502  om0r  8503  oaord1  8515  oaword1  8516  oaword2  8517  oawordeu  8519  oa00  8523  odi  8543  oeoa  8562  oeoe  8564  nna0r  8574  nnm0r  8575  naddrid  8649  naddlid  8650  naddword1  8657  card2on  9499  card2inf  9500  harcl  9504  cantnfvalf  9617  rankon  9750  cardon  9899  card0  9913  alephon  10022  alephgeom  10035  alephfplem1  10057  djufi  10140  cfon  10208  ttukeylem4  10466  ttukeylem7  10469  cfpwsdom  10539  inar1  10730  rankcf  10732  gruina  10773  ltsval2  27697  ltssolem1  27716  nosepnelem  27720  nodense  27733  nolt02o  27736  bdayon  27822  cuteq1  27887  old0  27909  made0  27933  old1  27935  mulsproplem2  28187  mulsproplem3  28188  mulsproplem4  28189  mulsproplem5  28190  mulsproplem6  28191  mulsproplem7  28192  mulsproplem8  28193  mulsproplem12  28197  mulsproplem13  28198  mulsproplem14  28199  precsexlem1  28277  precsexlem2  28278  bnj168  34990  r1wf  35356  fineqvnttrclse  35384  rdgprc0  36105  rankeq1o  36485  0hf  36491  nmulr0  36509  nmull0  36510  onsucconn  36762  onsucsuccmp  36768  finxp1o  37850  finxpreclem4  37852  harn0  43643  onexoegt  43785  ordeldif1o  43801  oe0suclim  43818  oaordnr  43837  nnoeomeqom  43853  oenass  43860  omabs2  43873  omcl3g  43875  naddcnff  43903  nadd2rabex  43927  safesnsupfiss  43955  safesnsupfidom1o  43957  safesnsupfilb  43958  0fno  43975  nlim1NEW  43982  aleph1min  44097  wfaxrep  45534  wfaxnul  45536