Theorem 0elon 6411

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 6410	. 2 ⊢ Ord ∅
2		0ex 5261	. . 3 ⊢ ∅ ∈ V
3	2	elon 6364	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ On

This proof depends on syntax axioms:   ∈ wcel 2145  ∅c0 4279  Ord word 6354  Oncon0 6355

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359

This theorem is used by:  inton  6415  onn0  6422  on0eqel  6481  orduninsuc  7843  onzsl  7846  peano1  7889  smofvon2  8348  tfrlem16  8385  rdg0n  8426  1on  8473  ordgt0ge1  8485  oa0  8508  om0  8509  oe0m  8510  oe0m0  8512  oe0  8514  oesuclem  8517  omcl  8528  oecl  8529  oa0r  8530  om0r  8531  oaord1  8543  oaword1  8544  oaword2  8545  oawordeu  8547  oa00  8551  odi  8571  oeoa  8590  oeoe  8592  nna0r  8602  nnm0r  8603  naddrid  8677  naddlid  8678  naddword1  8685  card2on  9532  card2inf  9533  harcl  9537  cantnfvalf  9650  rankon  9785  r1wf  9822  0hf  9898  cardon  10006  card0  10020  alephon  10129  alephgeom  10142  alephfplem1  10164  djufi  10246  cfon  10313  ttukeylem4  10571  ttukeylem7  10574  cfpwsdom  10650  inar1  10841  rankcf  10843  gruina  10884  ltsval2  27995  ltssolem1  28014  nosepnelem  28018  nodense  28031  nolt02o  28034  bdayon  28120  cuteq1  28185  old0  28207  made0  28231  old1  28233  mulsproplem2  28485  mulsproplem3  28486  mulsproplem4  28487  mulsproplem5  28488  mulsproplem6  28489  mulsproplem7  28490  mulsproplem8  28491  mulsproplem12  28495  mulsproplem13  28496  mulsproplem14  28497  precsexlem1  28575  precsexlem2  28576  bnj168  35344  fineqvnttrclse  35765  rdgprc0  36525  rankeq1o  36902  nmulr0  36914  nmull0  36915  nmulss1  36933  onsucconn  37196  onsucsuccmp  37202  finxp1o  38283  finxpreclem4  38285  harn0  44062  onexoegt  44204  ordeldif1o  44220  oe0suclim  44237  oaordnr  44256  nnoeomeqom  44272  oenass  44279  omabs2  44292  omcl3g  44294  naddcnff  44322  nadd2rabex  44346  safesnsupfiss  44374  safesnsupfidom1o  44376  safesnsupfilb  44377  0fno  44394  nlim1NEW  44401  aleph1min  44516  wfaxrep  45936  wfaxnul  45938