Theorem 0elon 6372

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 6371	. 2 ⊢ Ord ∅
2		0ex 5236	. . 3 ⊢ ∅ ∈ V
3	2	elon 6326	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 232	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2119  ∅c0 4268  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-tr 5187  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  inton  6376  onn0  6383  on0eqel  6442  orduninsuc  7790  onzsl  7793  peano1  7836  smofvon2  8293  tfrlem16  8329  rdg0n  8370  1on  8414  ordgt0ge1  8425  oa0  8448  om0  8449  oe0m  8450  oe0m0  8452  oe0  8454  oesuclem  8457  omcl  8468  oecl  8469  oa0r  8470  om0r  8471  oaord1  8483  oaword1  8484  oaword2  8485  oawordeu  8487  oa00  8491  odi  8511  oeoa  8530  oeoe  8532  nna0r  8542  nnm0r  8543  naddrid  8616  naddlid  8617  naddword1  8624  card2on  9466  card2inf  9467  harcl  9471  cantnfvalf  9584  rankon  9717  cardon  9866  card0  9880  alephon  9989  alephgeom  10002  alephfplem1  10024  djufi  10107  ttukeylem4  10432  ttukeylem7  10435  cfpwsdom  10505  inar1  10696  rankcf  10698  gruina  10739  ltsval2  27645  ltssolem1  27664  nosepnelem  27668  nodense  27681  nolt02o  27684  bdayon  27769  cuteq1  27834  old0  27856  made0  27880  old1  27882  mulsproplem2  28134  mulsproplem3  28135  mulsproplem4  28136  mulsproplem5  28137  mulsproplem6  28138  mulsproplem7  28139  mulsproplem8  28140  mulsproplem12  28144  mulsproplem13  28145  mulsproplem14  28146  precsexlem1  28224  precsexlem2  28225  bnj168  34920  r1wf  35284  fineqvnttrclse  35312  rdgprc0  36026  rankeq1o  36406  0hf  36412  onsucconn  36673  onsucsuccmp  36679  finxp1o  37761  finxpreclem4  37763  harn0  43554  onexoegt  43696  ordeldif1o  43712  oe0suclim  43729  oaordnr  43748  nnoeomeqom  43764  oenass  43771  omabs2  43784  omcl3g  43786  naddcnff  43814  nadd2rabex  43838  safesnsupfiss  43866  safesnsupfidom1o  43868  safesnsupfilb  43869  0fno  43886  nlim1NEW  43893  aleph1min  44008  wfaxrep  45445  wfaxnul  45447