Theorem a9e 1483

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 1302 through ax-14 1312 and ax-17 1317, all axioms other than ax-9 1307 are believed to be theorems of free logic, although the system without ax-9 1307 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 1307	. 2 |- -. A.x -. x = y
2		df-ex 1327	. 2 |- (E.x x = y <-> -. A.x -. x = y)
3	1, 2	mpbir 207	1 |- E.x x = y

Syntax hints:  -. wn 2  A.wal 1296   = wceq 1298  E.wex 1326

This theorem is referenced by:  equvini 1531  equviniOLD 1532  ax11v2 1585  equid1 1646  ax11eq 1754  ax11el 1755  ax11inda 1762  a12stdy1 1763  euequ1 1861  axext3OLD 1868  sbcbrgOLD 3391  axsep 3437  axsep2 3439  dtrucor2 3519  opelopabsbOLD 3565  relop 4113  dmi 4172  dmiOLD 4173  csbima12g 4276  dmsnop 4367  csbfv12g 4699  csboprgOLD 4911  1st2val 5038  2nd2val 5039  axextnd 6095  csbneggOLD 6521  bnj1468 13145  bnj1014 13374  bnj1326 13496  bnj1329 13497  bnj1418 13529  ax13dfeq 13865  subtr 15352  subtr2 15353  pm11.07 16321  ax10-16 16365

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

This theorem depends on definitions:  df-bi 164  df-ex 1327

Copyright terms: Public domain