Theorem 0elon 4392

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

Syntax hints:   ∈ wcel 2148  ∅c0 3422  Ord word 4362  Oncon0 4363

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-nul 4129

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-dif 3131  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-uni 3810  df-tr 4102  df-iord 4366  df-on 4368

This theorem is referenced by:  inton  4393  onn0  4400  onm  4401  limon  4512  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  onsucsssucexmid  4526  onsucelsucexmid  4529  ordsoexmid  4561  ordpwsucexmid  4569  ordtri2or2exmid  4570  ontri2orexmidim  4571  tfr0dm  6322  1on  6423  ordgt0ge1  6435  omv  6455  oa0  6457  om0  6458  oei0  6459  omcl  6461  omv2  6465  oaword1  6471  nna0r  6478  nnm0r  6479  card0  7186