Theorem exexneq

Description: There exist two different sets. (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	exexneq	$$⊢\exists x\exists y\neg x=y$$

Proof

Step	Hyp	Ref	Expression
1		exel	$$⊢\exists x\exists zz\in x$$
2		ax-nul	$$⊢\exists y\forall z\neg z\in y$$
3		exdistrv	$$⊢\exists x\exists y\left(\exists zz\in x\wedge \forall z\neg z\in y\right)\leftrightarrow \left(\exists x\exists zz\in x\wedge \exists y\forall z\neg z\in y\right)$$
4	1 2 3	mpbir2an	$$⊢\exists x\exists y\left(\exists zz\in x\wedge \forall z\neg z\in y\right)$$
5		ax9v1	$$⊢x=y\to \left(z\in x\to z\in y\right)$$
6	5	eximdv	$$⊢x=y\to \left(\exists zz\in x\to \exists zz\in y\right)$$
7		df-ex	$$⊢\exists zz\in y\leftrightarrow \neg \forall z\neg z\in y$$
8	6 7	imbitrdi	$$⊢x=y\to \left(\exists zz\in x\to \neg \forall z\neg z\in y\right)$$
9	8	com12	$$⊢\exists zz\in x\to \left(x=y\to \neg \forall z\neg z\in y\right)$$
10	9	con2d	$$⊢\exists zz\in x\to \left(\forall z\neg z\in y\to \neg x=y\right)$$
11	10	imp	$$⊢\left(\exists zz\in x\wedge \forall z\neg z\in y\right)\to \neg x=y$$
12	11	2eximi	$$⊢\exists x\exists y\left(\exists zz\in x\wedge \forall z\neg z\in y\right)\to \exists x\exists y\neg x=y$$
13	4 12	ax-mp	$$⊢\exists x\exists y\neg x=y$$