Theorem a9e 1125

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 960 through ax-14 970 and ax-17 971, all axioms other than ax-9 965 are believed to be theorems of free logic, although the system without ax-9 965 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 965	. 2 |- -. A.x -. x = y
2		df-ex 981	. 2 |- (E.x x = y <-> -. A.x -. x = y)
3	1, 2	mpbir 190	1 |- E.x x = y

Syntax hints:  -. wn 2  A.wal 954   = wceq 956  E.wex 980

This theorem is referenced by:  equvini 1168  ax11v2 1215  equid1 1269  ax11eq 1363  ax11el 1364  ax11inda 1371  a12stdy1 1372  zfext2 1461  sbcbrg 2662  axsep 2702  axsep2 2704  dtrucor2 2774  opabsb 2815  relop 3275  dmi 3326  csbima12g 3413  csbfv12g 3742  csboprg 3986  1st2val 4095  2nd2val 4096  ecelqsi 4292  axextnd 4943  csbnegg 5364

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

This theorem depends on definitions:  df-bi 147  df-ex 981

Copyright terms: Public domain