Theorem 0elon 6246

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 6245	. 2 ⊢ Ord ∅
2		0ex 5213	. . 3 ⊢ ∅ ∈ V
3	2	elon 6202	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 233	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2114  ∅c0 4293  Ord word 6192  Oncon0 6193

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954  df-nul 4294  df-pw 4543  df-uni 4841  df-tr 5175  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-ord 6196  df-on 6197

This theorem is referenced by:  inton  6250  onn0  6257  on0eqel  6310  orduninsuc  7560  onzsl  7563  smofvon2  7995  tfrlem16  8031  1on  8111  ordgt0ge1  8124  oa0  8143  om0  8144  oe0m  8145  oe0m0  8147  oe0  8149  oesuclem  8152  omcl  8163  oecl  8164  oa0r  8165  om0r  8166  oaord1  8179  oaword1  8180  oaword2  8181  oawordeu  8183  oa00  8187  odi  8207  oeoa  8225  oeoe  8227  nna0r  8237  nnm0r  8238  card2on  9020  card2inf  9021  harcl  9027  cantnfvalf  9130  rankon  9226  cardon  9375  card0  9389  alephon  9497  alephgeom  9510  alephfplem1  9532  djufi  9614  ttukeylem4  9936  ttukeylem7  9939  cfpwsdom  10008  inar1  10199  rankcf  10201  gruina  10242  bnj168  32002  rdgprc0  33040  sltval2  33165  sltsolem1  33182  nosepnelem  33186  nodense  33198  nolt02o  33201  bdayelon  33248  rankeq1o  33634  0hf  33640  onsucconn  33788  onsucsuccmp  33794  finxp1o  34675  finxpreclem4  34677  harn0  39709  aleph1min  39923