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 5185	. . 3 ⊢ ∅ ∈ V
3	2	elon 6200	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2112  ∅c0 4223  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 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-11 2160  ax-ext 2708  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-tr 5147  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-ord 6194  df-on 6195

This theorem is referenced by:  inton  6248  onn0  6255  on0eqel  6309  orduninsuc  7600  onzsl  7603  smofvon2  8071  tfrlem16  8107  1on  8187  ordgt0ge1  8202  oa0  8221  om0  8222  oe0m  8223  oe0m0  8225  oe0  8227  oesuclem  8230  omcl  8241  oecl  8242  oa0r  8243  om0r  8244  oaord1  8257  oaword1  8258  oaword2  8259  oawordeu  8261  oa00  8265  odi  8285  oeoa  8303  oeoe  8305  nna0r  8315  nnm0r  8316  card2on  9148  card2inf  9149  harcl  9153  cantnfvalf  9258  rankon  9376  cardon  9525  card0  9539  alephon  9648  alephgeom  9661  alephfplem1  9683  djufi  9765  ttukeylem4  10091  ttukeylem7  10094  cfpwsdom  10163  inar1  10354  rankcf  10356  gruina  10397  bnj168  32375  rdgprc0  33439  naddid1  33522  sltval2  33545  sltsolem1  33564  nosepnelem  33568  nodense  33581  nolt02o  33584  bdayelon  33657  old0  33729  made0  33743  rankeq1o  34159  0hf  34165  onsucconn  34313  onsucsuccmp  34319  finxp1o  35249  finxpreclem4  35251  harn0  40571  aleph1min  40781