Theorem a9e 1127

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 962 through ax-14 972 and ax-17 973, all axioms other than ax-9 967 are believed to be theorems of free logic, although the system without ax-9 967 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 967	. 2 |- -. A.x -. x = y
2		df-ex 983	. 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 956   = wceq 958  E.wex 982

This theorem is referenced by:  equvini 1170  ax11v2 1217  equid1 1271  ax11eq 1365  ax11el 1366  ax11inda 1373  a12stdy1 1374  zfext2 1464  sbcbrg 2667  axsep 2707  axsep2 2709  dtrucor2 2780  opabsb 2821  relop 3281  dmi 3332  csbima12g 3419  csbfv12g 3748  csboprg 3992  1st2val 4101  2nd2val 4102  ecelqsi 4298  axextnd 4955  csbnegg 5376

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

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

Copyright terms: Public domain