Theorem ax6e

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-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.)

	Ref	Expression
Assertion	ax6e	$$⊢\exists xx=y$$

Proof

Step	Hyp	Ref	Expression
1		19.8a	$$⊢x=y\to \exists xx=y$$
2		ax13lem1	$$⊢\neg x=y\to \left(w=y\to \forall xw=y\right)$$
3		ax6ev	$$⊢\exists xx=w$$
4		equtr	$$⊢x=w\to \left(w=y\to x=y\right)$$
5	3 4	eximii	$$⊢\exists x\left(w=y\to x=y\right)$$
6	5	19.35i	$$⊢\forall xw=y\to \exists xx=y$$
7	2 6	syl6com	$$⊢w=y\to \left(\neg x=y\to \exists xx=y\right)$$
8		ax6ev	$$⊢\exists ww=y$$
9	7 8	exlimiiv	$$⊢\neg x=y\to \exists xx=y$$
10	1 9	pm2.61i	$$⊢\exists xx=y$$