Theorem 0elon 6390

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

Syntax hints:   ∈ wcel 2109  ∅c0 4299  Ord word 6334  Oncon0 6335

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 2702  ax-nul 5264

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-tr 5218  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  inton  6394  onn0  6401  on0eqel  6461  orduninsuc  7822  onzsl  7825  peano1  7868  smofvon2  8328  tfrlem16  8364  rdg0n  8405  1on  8449  ordgt0ge1  8460  oa0  8483  om0  8484  oe0m  8485  oe0m0  8487  oe0  8489  oesuclem  8492  omcl  8503  oecl  8504  oa0r  8505  om0r  8506  oaord1  8518  oaword1  8519  oaword2  8520  oawordeu  8522  oa00  8526  odi  8546  oeoa  8564  oeoe  8566  nna0r  8576  nnm0r  8577  naddrid  8650  naddlid  8651  naddword1  8658  card2on  9514  card2inf  9515  harcl  9519  cantnfvalf  9625  rankon  9755  cardon  9904  card0  9918  alephon  10029  alephgeom  10042  alephfplem1  10064  djufi  10147  ttukeylem4  10472  ttukeylem7  10475  cfpwsdom  10544  inar1  10735  rankcf  10737  gruina  10778  sltval2  27575  sltsolem1  27594  nosepnelem  27598  nodense  27611  nolt02o  27614  bdayelon  27695  cuteq1  27753  old0  27774  made0  27792  old1  27794  mulsproplem2  28027  mulsproplem3  28028  mulsproplem4  28029  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  precsexlem1  28116  precsexlem2  28117  bnj168  34727  rdgprc0  35788  rankeq1o  36166  0hf  36172  onsucconn  36433  onsucsuccmp  36439  finxp1o  37387  finxpreclem4  37389  harn0  43098  onexoegt  43240  ordeldif1o  43256  oe0suclim  43273  oaordnr  43292  nnoeomeqom  43308  oenass  43315  omabs2  43328  omcl3g  43330  naddcnff  43358  nadd2rabex  43382  safesnsupfiss  43411  safesnsupfidom1o  43413  safesnsupfilb  43414  0no  43431  nlim1NEW  43438  aleph1min  43553  wfaxrep  44991  wfaxnul  44993