Theorem a9e 1556

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 1336 through ax-14 1396 and ax-17 1402, all axioms other than ax-9 1418 are believed to be theorems of free logic, although the system without ax-9 1418 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-i9 1417	1 |- E.x x = y

Syntax hints:  E.wex 1374

This theorem is referenced by:  ax9o  1557  equid1  1561  equs4  1582  equsex  1584  a4ime  1593  equvini  1602  ax11v2  1651  pm11.07  1783  ax11eq  1810  ax11el  1811  ax11inda  1818  a12stdy1  1819  euequ1  1912

This theorem was proved from axioms:  ax-i9 1417