Theorem 0elon 4488

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 4487	. 2 ⊢ Ord ∅
2		0ex 4215	. . 3 ⊢ ∅ ∈ V
3	2	elon 4470	. 2 ⊢ (∅ ∈ On ↔ Ord ∅)
4	1, 3	mpbir 146	1 ⊢ ∅ ∈ On

Syntax hints:   ∈ wcel 2201  ∅c0 3493  Ord word 4458  Oncon0 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-nul 4214

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-dif 3201  df-in 3205  df-ss 3212  df-nul 3494  df-pw 3653  df-uni 3893  df-tr 4187  df-iord 4462  df-on 4464

This theorem is referenced by:  inton  4489  onn0  4496  onm  4497  limon  4610  ordtriexmid  4618  ontriexmidim  4619  ordtri2orexmid  4620  onsucsssucexmid  4624  onsucelsucexmid  4627  ordsoexmid  4659  ordpwsucexmid  4667  ordtri2or2exmid  4668  ontri2orexmidim  4669  tfr0dm  6490  1on  6591  ordgt0ge1  6605  omv  6625  oa0  6627  om0  6628  oei0  6629  omcl  6631  omv2  6635  oaword1  6641  nna0r  6648  nnm0r  6649  card0  7394