Theorem 0elon 4394

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	|- (/) e. On

Proof of Theorem 0elon

Step	Hyp	Ref	Expression
1		ord0 4393	. 2 |- Ord (/)
2		0ex 4132	. . 3 |- (/) e. _V
3	2	elon 4376	. 2 |- ( (/) e. On <-> Ord (/) )
4	1, 3	mpbir 146	1 |- (/) e. On

Syntax hints:   e. wcel 2148   (/)c0 3424   Ord word 4364   Oncon0 4365

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 4131

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 2741  df-dif 3133  df-in 3137  df-ss 3144  df-nul 3425  df-pw 3579  df-uni 3812  df-tr 4104  df-iord 4368  df-on 4370

This theorem is referenced by:  inton  4395  onn0  4402  onm  4403  limon  4514  ordtriexmid  4522  ontriexmidim  4523  ordtri2orexmid  4524  onsucsssucexmid  4528  onsucelsucexmid  4531  ordsoexmid  4563  ordpwsucexmid  4571  ordtri2or2exmid  4572  ontri2orexmidim  4573  tfr0dm  6325  1on  6426  ordgt0ge1  6438  omv  6458  oa0  6460  om0  6461  oei0  6462  omcl  6464  omv2  6468  oaword1  6474  nna0r  6481  nnm0r  6482  card0  7189