Theorem a9e 1166

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 1001 through ax-14 1011 and ax-17 1012, all axioms other than ax-9 1006 are believed to be theorems of free logic, although the system without ax-9 1006 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 1006	. 2 |- -. A.x -. x = y
2		df-ex 1022	. 2 |- (E.x x = y <-> -. A.x -. x = y)
3	1, 2	mpbir 197	1 |- E.x x = y

Syntax hints:  -. wn 2  A.wal 995   = wceq 997  E.wex 1021

This theorem is referenced by:  equvini 1210  ax11v2 1257  equid1 1311  ax11eq 1405  ax11el 1406  ax11inda 1413  a12stdy1 1414  euequ1 1500  euequ1OLD 1501  axext3 1506  sbcbrg 2717  axsep 2757  axsep2 2759  dtrucor2 2830  opelopabsb 2871  relop 3332  dmi 3383  csbima12g 3470  csbfv12g 3799  csboprg 4044  1st2val 4153  2nd2val 4154  ecelqsi 4352  axextnd 5008  csbnegg 5429

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

This theorem depends on definitions:  df-bi 154  df-ex 1022

Copyright terms: Public domain