Theorem a9e 1707

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

Assertion

Ref	Expression
a9e	⊢ ∃𝑥 𝑥 = 𝑦

Proof of Theorem a9e

Step	Hyp	Ref	Expression
1		ax-i9 1541	1 ⊢ ∃𝑥 𝑥 = 𝑦

Syntax hints:  ∃wex 1503

This theorem was proved from axioms:  ax-i9 1541

This theorem is referenced by:  ax9o  1709  equid  1712  equs4  1736  equsal  1738  equsex  1739  equsexd  1740  spimt  1747  spimeh  1750  spimed  1751  equvini  1769  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  euequ1  2133