Theorem 0elon 6366

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

Syntax hints:   ∈ wcel 2109  ∅c0 4286  Ord word 6310  Oncon0 6311

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 5248

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-tr 5203  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-ord 6314  df-on 6315

This theorem is referenced by:  inton  6370  onn0  6377  on0eqel  6436  orduninsuc  7783  onzsl  7786  peano1  7829  smofvon2  8286  tfrlem16  8322  rdg0n  8363  1on  8407  ordgt0ge1  8418  oa0  8441  om0  8442  oe0m  8443  oe0m0  8445  oe0  8447  oesuclem  8450  omcl  8461  oecl  8462  oa0r  8463  om0r  8464  oaord1  8476  oaword1  8477  oaword2  8478  oawordeu  8480  oa00  8484  odi  8504  oeoa  8522  oeoe  8524  nna0r  8534  nnm0r  8535  naddrid  8608  naddlid  8609  naddword1  8616  card2on  9465  card2inf  9466  harcl  9470  cantnfvalf  9580  rankon  9710  cardon  9859  card0  9873  alephon  9982  alephgeom  9995  alephfplem1  10017  djufi  10100  ttukeylem4  10425  ttukeylem7  10428  cfpwsdom  10497  inar1  10688  rankcf  10690  gruina  10731  sltval2  27584  sltsolem1  27603  nosepnelem  27607  nodense  27620  nolt02o  27623  bdayelon  27704  cuteq1  27766  old0  27787  made0  27805  old1  27807  mulsproplem2  28043  mulsproplem3  28044  mulsproplem4  28045  mulsproplem5  28046  mulsproplem6  28047  mulsproplem7  28048  mulsproplem8  28049  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  precsexlem1  28132  precsexlem2  28133  bnj168  34699  rdgprc0  35769  rankeq1o  36147  0hf  36153  onsucconn  36414  onsucsuccmp  36420  finxp1o  37368  finxpreclem4  37370  harn0  43078  onexoegt  43220  ordeldif1o  43236  oe0suclim  43253  oaordnr  43272  nnoeomeqom  43288  oenass  43295  omabs2  43308  omcl3g  43310  naddcnff  43338  nadd2rabex  43362  safesnsupfiss  43391  safesnsupfidom1o  43393  safesnsupfilb  43394  0no  43411  nlim1NEW  43418  aleph1min  43533  wfaxrep  44971  wfaxnul  44973