Theorem 0elon 4393

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

Syntax hints:   ∈ wcel 2148  ∅c0 3423  Ord word 4363  Oncon0 4364

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 4130

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 2740  df-dif 3132  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-uni 3811  df-tr 4103  df-iord 4367  df-on 4369

This theorem is referenced by:  inton  4394  onn0  4401  onm  4402  limon  4513  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  onsucsssucexmid  4527  onsucelsucexmid  4530  ordsoexmid  4562  ordpwsucexmid  4570  ordtri2or2exmid  4571  ontri2orexmidim  4572  tfr0dm  6323  1on  6424  ordgt0ge1  6436  omv  6456  oa0  6458  om0  6459  oei0  6460  omcl  6462  omv2  6466  oaword1  6472  nna0r  6479  nnm0r  6480  card0  7187