Theorem 0elon 6244

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

Syntax hints:   ∈ wcel 2114  ∅c0 4291  Ord word 6190  Oncon0 6191

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 2793  ax-nul 5210

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-uni 4839  df-tr 5173  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195

This theorem is referenced by:  inton  6248  onn0  6255  on0eqel  6308  orduninsuc  7558  onzsl  7561  smofvon2  7993  tfrlem16  8029  1on  8109  ordgt0ge1  8122  oa0  8141  om0  8142  oe0m  8143  oe0m0  8145  oe0  8147  oesuclem  8150  omcl  8161  oecl  8162  oa0r  8163  om0r  8164  oaord1  8177  oaword1  8178  oaword2  8179  oawordeu  8181  oa00  8185  odi  8205  oeoa  8223  oeoe  8225  nna0r  8235  nnm0r  8236  card2on  9018  card2inf  9019  harcl  9025  cantnfvalf  9128  rankon  9224  cardon  9373  card0  9387  alephon  9495  alephgeom  9508  alephfplem1  9530  djufi  9612  ttukeylem4  9934  ttukeylem7  9937  cfpwsdom  10006  inar1  10197  rankcf  10199  gruina  10240  bnj168  32000  rdgprc0  33038  sltval2  33163  sltsolem1  33180  nosepnelem  33184  nodense  33196  nolt02o  33199  bdayelon  33246  rankeq1o  33632  0hf  33638  onsucconn  33786  onsucsuccmp  33792  finxp1o  34676  finxpreclem4  34678  harn0  39751  aleph1min  39965