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 5252	. . 3 ⊢ ∅ ∈ V
3	2	elon 6326	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2113  ∅c0 4285  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-tr 5206  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321

This theorem is referenced by:  inton  6376  onn0  6383  on0eqel  6442  orduninsuc  7785  onzsl  7788  peano1  7831  smofvon2  8288  tfrlem16  8324  rdg0n  8365  1on  8409  ordgt0ge1  8420  oa0  8443  om0  8444  oe0m  8445  oe0m0  8447  oe0  8449  oesuclem  8452  omcl  8463  oecl  8464  oa0r  8465  om0r  8466  oaord1  8478  oaword1  8479  oaword2  8480  oawordeu  8482  oa00  8486  odi  8506  oeoa  8525  oeoe  8527  nna0r  8537  nnm0r  8538  naddrid  8611  naddlid  8612  naddword1  8619  card2on  9459  card2inf  9460  harcl  9464  cantnfvalf  9574  rankon  9707  cardon  9856  card0  9870  alephon  9979  alephgeom  9992  alephfplem1  10014  djufi  10097  ttukeylem4  10422  ttukeylem7  10425  cfpwsdom  10495  inar1  10686  rankcf  10688  gruina  10729  ltsval2  27624  ltssolem1  27643  nosepnelem  27647  nodense  27660  nolt02o  27663  bdayon  27748  cuteq1  27813  old0  27835  made0  27859  old1  27861  mulsproplem2  28113  mulsproplem3  28114  mulsproplem4  28115  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  precsexlem1  28203  precsexlem2  28204  bnj168  34886  r1wf  35252  fineqvnttrclse  35280  rdgprc0  35985  rankeq1o  36365  0hf  36371  onsucconn  36632  onsucsuccmp  36638  finxp1o  37593  finxpreclem4  37595  harn0  43340  onexoegt  43482  ordeldif1o  43498  oe0suclim  43515  oaordnr  43534  nnoeomeqom  43550  oenass  43557  omabs2  43570  omcl3g  43572  naddcnff  43600  nadd2rabex  43624  safesnsupfiss  43652  safesnsupfidom1o  43654  safesnsupfilb  43655  0fno  43672  nlim1NEW  43679  aleph1min  43794  wfaxrep  45231  wfaxnul  45233