Theorem 0elon 6304

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 6303	. 2 ⊢ Ord ∅
2		0ex 5226	. . 3 ⊢ ∅ ∈ V
3	2	elon 6260	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 230	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2108  ∅c0 4253  Ord word 6250  Oncon0 6251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-tr 5188  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-ord 6254  df-on 6255

This theorem is referenced by:  inton  6308  onn0  6315  on0eqel  6369  orduninsuc  7665  onzsl  7668  smofvon2  8158  tfrlem16  8195  1on  8274  ordgt0ge1  8289  oa0  8308  om0  8309  oe0m  8310  oe0m0  8312  oe0  8314  oesuclem  8317  omcl  8328  oecl  8329  oa0r  8330  om0r  8331  oaord1  8344  oaword1  8345  oaword2  8346  oawordeu  8348  oa00  8352  odi  8372  oeoa  8390  oeoe  8392  nna0r  8402  nnm0r  8403  card2on  9243  card2inf  9244  harcl  9248  cantnfvalf  9353  rankon  9484  cardon  9633  card0  9647  alephon  9756  alephgeom  9769  alephfplem1  9791  djufi  9873  ttukeylem4  10199  ttukeylem7  10202  cfpwsdom  10271  inar1  10462  rankcf  10464  gruina  10505  bnj168  32609  rdg0n  33598  rdgprc0  33675  naddid1  33763  sltval2  33786  sltsolem1  33805  nosepnelem  33809  nodense  33822  nolt02o  33825  bdayelon  33898  old0  33970  made0  33984  rankeq1o  34400  0hf  34406  onsucconn  34554  onsucsuccmp  34560  finxp1o  35490  finxpreclem4  35492  harn0  40843  aleph1min  41053