Theorem 0elon 4352

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 4351	. 2 ⊢ Ord ∅
2		0ex 4091	. . 3 ⊢ ∅ ∈ V
3	2	elon 4334	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 145	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2128  ∅c0 3394  Ord word 4322  Oncon0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-nul 4090

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-dif 3104  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-uni 3773  df-tr 4063  df-iord 4326  df-on 4328

This theorem is referenced by:  inton  4353  onn0  4360  onm  4361  limon  4472  ordtriexmid  4480  ontriexmidim  4481  ordtri2orexmid  4482  onsucsssucexmid  4486  onsucelsucexmid  4489  ordsoexmid  4521  ordpwsucexmid  4529  ordtri2or2exmid  4530  ontri2orexmidim  4531  tfr0dm  6269  1on  6370  ordgt0ge1  6382  omv  6402  oa0  6404  om0  6405  oei0  6406  omcl  6408  omv2  6412  oaword1  6418  nna0r  6425  nnm0r  6426  card0  7123