Theorem 0elon 5816

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 5815	. 2 ⊢ Ord ∅
2		0ex 4823	. . 3 ⊢ ∅ ∈ V
3	2	elon 5770	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 221	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2030  ∅c0 3948  Ord word 5760  Oncon0 5761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949  df-pw 4193  df-uni 4469  df-tr 4786  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-ord 5764  df-on 5765

This theorem is referenced by:  inton  5820  onn0  5827  on0eqel  5883  orduninsuc  7085  onzsl  7088  smofvon2  7498  tfrlem16  7534  1on  7612  ordgt0ge1  7622  oa0  7641  om0  7642  oe0m  7643  oe0m0  7645  oe0  7647  oesuclem  7650  omcl  7661  oecl  7662  oa0r  7663  om0r  7664  oaord1  7676  oaword1  7677  oaword2  7678  oawordeu  7680  oa00  7684  odi  7704  oeoa  7722  oeoe  7724  nna0r  7734  nnm0r  7735  card2on  8500  card2inf  8501  harcl  8507  cantnfvalf  8600  rankon  8696  cardon  8808  card0  8822  alephon  8930  alephgeom  8943  alephfplem1  8965  cdafi  9050  ttukeylem4  9372  ttukeylem7  9375  cfpwsdom  9444  inar1  9635  rankcf  9637  gruina  9678  bnj168  30924  rdgprc0  31823  sltval2  31934  sltsolem1  31951  nosepnelem  31955  nodense  31967  nolt02o  31970  bdayelon  32017  rankeq1o  32403  0hf  32409  onsucconn  32562  onsucsuccmp  32568  finxp1o  33359  finxpreclem4  33361  harn0  37989