Theorem a9e 1161

Description: At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 996 through ax-14 1006 and ax-17 1007, all axioms other than ax-9 1001 are believed to be theorems of free logic, although the system without ax-9 1001 is probably not complete in free logic.

Assertion

Ref	Expression
a9e	|- E.x x = y

Proof of Theorem a9e

Step	Hyp	Ref	Expression
1		ax-9 1001	. 2 |- -. A.x -. x = y
2		df-ex 1017	. 2 |- (E.x x = y <-> -. A.x -. x = y)
3	1, 2	mpbir 188	1 |- E.x x = y

Syntax hints:  -. wn 2  A.wal 990   = wceq 992  E.wex 1016

This theorem is referenced by:  equvini 1205  ax11v2 1252  equid1 1307  ax11eq 1402  ax11el 1403  ax11inda 1410  a12stdy1 1411  euequ1 1497  axext3 1502  sbcbrg 2736  axsep 2776  axsep2 2778  dtrucor2 2850  opelopabsb 2892  relop 3365  dmi 3415  csbima12g 3505  csbfv12g 3853  csboprg 4044  1st2val 4158  2nd2val 4159  axextnd 5097  csbnegg 5518  subtr 11395  subtr2 11396

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-9 1001

This theorem depends on definitions:  df-bi 145  df-ex 1017

Copyright terms: Public domain