Theorem exneq

Description: Given any set (the " y " in the statement), there exists a set not equal to it.

The same statement without disjoint variable condition is false, since we do not have E. x -. x = x . This theorem is proved directly from set theory axioms (no class definitions) and does not depend on ax-ext , ax-sep , or ax-pow nor auxiliary logical axiom schemes ax-10 to ax-13 . See dtruALT for a shorter proof using more axioms, and dtruALT2 for a proof using ax-pow instead of ax-pr . (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by BJ, 31-May-2019) Avoid ax-8 . (Revised by SN, 21-Sep-2023) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) Use ax-pr instead of ax-pow . (Revised by BTernaryTau, 3-Dec-2024) Extract this result from the proof of dtru . (Revised by BJ, 2-Jan-2025)

	Ref	Expression
Assertion	exneq	$$⊢\exists x\neg x=y$$

Proof

Step	Hyp	Ref	Expression
1		exexneq	$$⊢\exists z\exists w\neg z=w$$
2		equeuclr	$$⊢w=y\to \left(z=y\to z=w\right)$$
3	2	con3d	$$⊢w=y\to \left(\neg z=w\to \neg z=y\right)$$
4		ax7v1	$$⊢x=z\to \left(x=y\to z=y\right)$$
5	4	con3d	$$⊢x=z\to \left(\neg z=y\to \neg x=y\right)$$
6	5	spimevw	$$⊢\neg z=y\to \exists x\neg x=y$$
7	3 6	syl6	$$⊢w=y\to \left(\neg z=w\to \exists x\neg x=y\right)$$
8		ax7v1	$$⊢x=w\to \left(x=y\to w=y\right)$$
9	8	con3d	$$⊢x=w\to \left(\neg w=y\to \neg x=y\right)$$
10	9	spimevw	$$⊢\neg w=y\to \exists x\neg x=y$$
11	10	a1d	$$⊢\neg w=y\to \left(\neg z=w\to \exists x\neg x=y\right)$$
12	7 11	pm2.61i	$$⊢\neg z=w\to \exists x\neg x=y$$
13	12	exlimivv	$$⊢\exists z\exists w\neg z=w\to \exists x\neg x=y$$
14	1 13	ax-mp	$$⊢\exists x\neg x=y$$