Theorem 0elon 3017

Description: The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193.

Assertion

Ref	Expression
0elon	|- (/) e. On

Proof of Theorem 0elon

Step	Hyp	Ref	Expression
1		ord0 3016	. 2 |- Ord (/)
2		0ex 2706	. . 3 |- (/) e. V
3	2	elon 2952	. 2 |- ((/) e. On <-> Ord (/))
4	1, 3	mpbir 190	1 |- (/) e. On

Syntax hints:   e. wcel 956  (/)c0 2276  Ord word 2942  Oncon0 2943

This theorem is referenced by:  inton 3021  onne0 3028  orduninsuc 3109  on0eqelt 3119  tz7.44-1 3919  rdgsuct 3936  rdglimt 3939  1on 4128  ordgt0ge1 4134  oa0 4145  om0 4146  oe0m 4147  oe0m0 4149  oe0 4151  oa1suc 4154  oesuc 4156  omcl 4161  oecl 4162  oa0r 4163  om0r 4164  om1 4166  oe1 4168  oaord1 4175  oaword1 4176  oaword2 4177  oawordeu 4179  oa00 4183  odi 4200  rankon 4651  rankeq0 4676  numth2 4765  card0 4803  alephon 4845  alephgeom 4862  alephfplem1 4876  cdafi 4916

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-nul 2705

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-tr 2676  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947

Copyright terms: Public domain