Theorem a9e 1744

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 1495 through ax-14 2205 and ax-17 1574, all axioms other than ax-9 1579 are believed to be theorems of free logic, although the system without ax-9 1579 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)

Assertion

Ref	Expression
a9e	|- E. x x = y

Proof of Theorem a9e

Step	Hyp	Ref	Expression
1		ax-i9 1578	1 |- E. x x = y

Syntax hints:   E.wex 1540

This theorem was proved from axioms:  ax-i9 1578

This theorem is referenced by:  ax9o  1746  equid  1749  equs4  1773  equsal  1775  equsex  1776  equsexd  1777  spimt  1784  spimeh  1787  spimed  1788  equvini  1806  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  euequ1  2175