Theorem 0elon 6387

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

Syntax hints:   ∈ wcel 2109  ∅c0 4296  Ord word 6331  Oncon0 6332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-tr 5215  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  inton  6391  onn0  6398  on0eqel  6458  orduninsuc  7819  onzsl  7822  peano1  7865  smofvon2  8325  tfrlem16  8361  rdg0n  8402  1on  8446  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  8561  oeoe  8563  nna0r  8573  nnm0r  8574  naddrid  8647  naddlid  8648  naddword1  8655  card2on  9507  card2inf  9508  harcl  9512  cantnfvalf  9618  rankon  9748  cardon  9897  card0  9911  alephon  10022  alephgeom  10035  alephfplem1  10057  djufi  10140  ttukeylem4  10465  ttukeylem7  10468  cfpwsdom  10537  inar1  10728  rankcf  10730  gruina  10771  sltval2  27568  sltsolem1  27587  nosepnelem  27591  nodense  27604  nolt02o  27607  bdayelon  27688  cuteq1  27746  old0  27767  made0  27785  old1  27787  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  precsexlem1  28109  precsexlem2  28110  bnj168  34720  rdgprc0  35781  rankeq1o  36159  0hf  36165  onsucconn  36426  onsucsuccmp  36432  finxp1o  37380  finxpreclem4  37382  harn0  43091  onexoegt  43233  ordeldif1o  43249  oe0suclim  43266  oaordnr  43285  nnoeomeqom  43301  oenass  43308  omabs2  43321  omcl3g  43323  naddcnff  43351  nadd2rabex  43375  safesnsupfiss  43404  safesnsupfidom1o  43406  safesnsupfilb  43407  0no  43424  nlim1NEW  43431  aleph1min  43546  wfaxrep  44984  wfaxnul  44986