Theorem 0elon 6319

Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)

Assertion

Ref	Expression
0elon	⊢ ∅ ∈ On

Proof of Theorem 0elon

Step	Hyp	Ref	Expression
1		ord0 6318	. 2 ⊢ Ord ∅
2		0ex 5231	. . 3 ⊢ ∅ ∈ V
3	2	elon 6275	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 230	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2106  ∅c0 4256  Ord word 6265  Oncon0 6266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-tr 5192  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270

This theorem is referenced by:  inton  6323  onn0  6330  on0eqel  6384  orduninsuc  7690  onzsl  7693  peano1  7735  smofvon2  8187  tfrlem16  8224  rdg0n  8265  1on  8309  1onOLD  8310  ordgt0ge1  8323  oa0  8346  om0  8347  oe0m  8348  oe0m0  8350  oe0  8352  oesuclem  8355  omcl  8366  oecl  8367  oa0r  8368  om0r  8369  oaord1  8382  oaword1  8383  oaword2  8384  oawordeu  8386  oa00  8390  odi  8410  oeoa  8428  oeoe  8430  nna0r  8440  nnm0r  8441  card2on  9313  card2inf  9314  harcl  9318  cantnfvalf  9423  rankon  9553  cardon  9702  card0  9716  alephon  9825  alephgeom  9838  alephfplem1  9860  djufi  9942  ttukeylem4  10268  ttukeylem7  10271  cfpwsdom  10340  inar1  10531  rankcf  10533  gruina  10574  bnj168  32709  rdgprc0  33769  naddid1  33836  sltval2  33859  sltsolem1  33878  nosepnelem  33882  nodense  33895  nolt02o  33898  bdayelon  33971  old0  34043  made0  34057  rankeq1o  34473  0hf  34479  onsucconn  34627  onsucsuccmp  34633  finxp1o  35563  finxpreclem4  35565  harn0  40927  nlim1NEW  41049  aleph1min  41164