Theorem ax6e

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-4] through [ax-9], all axioms other than [ax-6] are believed to be theorems of free logic, although the system without [ax-6] is not complete in free logic.

Usage of this theorem is discouraged because it depends on [ax-13]. It is preferred to use ax6ev when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)

Conclusion
\( \vdash \exists x \, x = y' \)
Proof
l0
19.8a
\( \vdash x = y' \rightarrow \exists x \, x = y' \)
l1
ax13lem1
\( \vdash \neg x = y' \rightarrow w = y' \rightarrow \forall x \, w = y' \)
l2
ax6ev
\( \vdash \exists x \, x = w \)
equtr
\( \vdash x = w \rightarrow w = y' \rightarrow x = y' \)
eximii l2 _
19.35i _
\( \vdash \forall x \, w = y' \rightarrow \exists x \, x = y' \)
l6
syl6com l1 _
\( \vdash w = y' \rightarrow \neg x = y' \rightarrow \exists x \, x = y' \)
ax6ev
\( \vdash \exists w \, w = y' \)
exlimiiv l6 _
\( \vdash \neg x = y' \rightarrow \exists x \, x = y' \)
pm2.61i l0 _