Theorem 0elon 6119

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

Syntax hints:   ∈ wcel 2081  ∅c0 4211  Ord word 6065  Oncon0 6066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-in 3866  df-ss 3874  df-nul 4212  df-pw 4455  df-uni 4746  df-tr 5064  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-ord 6069  df-on 6070

This theorem is referenced by:  inton  6123  onn0  6130  on0eqel  6183  orduninsuc  7414  onzsl  7417  smofvon2  7845  tfrlem16  7881  1on  7960  ordgt0ge1  7973  oa0  7992  om0  7993  oe0m  7994  oe0m0  7996  oe0  7998  oesuclem  8001  omcl  8012  oecl  8013  oa0r  8014  om0r  8015  oaord1  8027  oaword1  8028  oaword2  8029  oawordeu  8031  oa00  8035  odi  8055  oeoa  8073  oeoe  8075  nna0r  8085  nnm0r  8086  card2on  8864  card2inf  8865  harcl  8871  cantnfvalf  8974  rankon  9070  cardon  9219  card0  9233  alephon  9341  alephgeom  9354  alephfplem1  9376  djufi  9458  ttukeylem4  9780  ttukeylem7  9783  cfpwsdom  9852  inar1  10043  rankcf  10045  gruina  10086  bnj168  31617  rdgprc0  32647  sltval2  32772  sltsolem1  32789  nosepnelem  32793  nodense  32805  nolt02o  32808  bdayelon  32855  rankeq1o  33241  0hf  33247  onsucconn  33395  onsucsuccmp  33401  finxp1o  34204  finxpreclem4  34206  harn0  39187  aleph1min  39401