Theorem 0elon 6362

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

Syntax hints:   ∈ wcel 2109  ∅c0 4284  Ord word 6306  Oncon0 6307

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 5245

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-tr 5200  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  inton  6366  onn0  6373  on0eqel  6432  orduninsuc  7776  onzsl  7779  peano1  7822  smofvon2  8279  tfrlem16  8315  rdg0n  8356  1on  8400  ordgt0ge1  8411  oa0  8434  om0  8435  oe0m  8436  oe0m0  8438  oe0  8440  oesuclem  8443  omcl  8454  oecl  8455  oa0r  8456  om0r  8457  oaord1  8469  oaword1  8470  oaword2  8471  oawordeu  8473  oa00  8477  odi  8497  oeoa  8515  oeoe  8517  nna0r  8527  nnm0r  8528  naddrid  8601  naddlid  8602  naddword1  8609  card2on  9446  card2inf  9447  harcl  9451  cantnfvalf  9561  rankon  9691  cardon  9840  card0  9854  alephon  9963  alephgeom  9976  alephfplem1  9998  djufi  10081  ttukeylem4  10406  ttukeylem7  10409  cfpwsdom  10478  inar1  10669  rankcf  10671  gruina  10712  sltval2  27566  sltsolem1  27585  nosepnelem  27589  nodense  27602  nolt02o  27605  bdayelon  27686  cuteq1  27748  old0  27769  made0  27787  old1  27789  mulsproplem2  28025  mulsproplem3  28026  mulsproplem4  28027  mulsproplem5  28028  mulsproplem6  28029  mulsproplem7  28030  mulsproplem8  28031  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  precsexlem1  28114  precsexlem2  28115  bnj168  34697  rdgprc0  35767  rankeq1o  36145  0hf  36151  onsucconn  36412  onsucsuccmp  36418  finxp1o  37366  finxpreclem4  37368  harn0  43075  onexoegt  43217  ordeldif1o  43233  oe0suclim  43250  oaordnr  43269  nnoeomeqom  43285  oenass  43292  omabs2  43305  omcl3g  43307  naddcnff  43335  nadd2rabex  43359  safesnsupfiss  43388  safesnsupfidom1o  43390  safesnsupfilb  43391  0no  43408  nlim1NEW  43415  aleph1min  43530  wfaxrep  44968  wfaxnul  44970