Theorem 0elon 3079

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 3078	. 2 |- Ord (/)
2		0ex 2766	. . 3 |- (/) e. V
3	2	elon 3014	. 2 |- ((/) e. On <-> Ord (/))
4	1, 3	mpbir 197	1 |- (/) e. On

Syntax hints:   e. wcel 999  (/)c0 2331  Ord word 3004  Oncon0 3005

This theorem is referenced by:  inton 3083  onne0 3090  orduninsuc 3171  on0eqel 3181  tz7.44-1 3986  rdgsuc 4003  rdglim 4006  1on 4196  ordgt0ge1 4202  oa0 4213  om0 4214  oe0m 4215  oe0m0 4217  oe0 4219  oa1suc 4222  oesuc 4224  omcl 4229  oecl 4230  oa0r 4231  om0r 4232  om1 4234  oe1 4236  oaord1 4243  oaword1 4244  oaword2 4245  oawordeu 4247  oa00 4251  odi 4268  rankon 4733  rankeq0 4758  numth2 4847  card0 4885  alephon 4930  alephgeom 4947  alephfplem1 4961  cdafi 5001

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-nul 2765

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-tr 2736  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009

Copyright terms: Public domain