Theorem 2ax6elem

Description: We can always find values matching x and y , as long as they are represented by distinct variables. This theorem merges two ax6e instances E. z z = x and E. w w = y into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Wolf Lammen, 27-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	2ax6elem	$$⊢\neg \forall ww=z\to \exists z\exists w\left(z=x\wedge w=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax6e	$$⊢\exists zz=x$$
2		nfnae	$$⊢Ⅎz\neg \forall ww=z$$
3		nfnae	$$⊢Ⅎz\neg \forall ww=x$$
4	2 3	nfan	$$⊢Ⅎz\left(\neg \forall ww=z\wedge \neg \forall ww=x\right)$$
5		nfeqf	$$⊢\left(\neg \forall ww=z\wedge \neg \forall ww=x\right)\to Ⅎwz=x$$
6		pm3.21	$$⊢w=y\to \left(z=x\to \left(z=x\wedge w=y\right)\right)$$
7	5 6	spimed	$$⊢\left(\neg \forall ww=z\wedge \neg \forall ww=x\right)\to \left(z=x\to \exists w\left(z=x\wedge w=y\right)\right)$$
8	4 7	eximd	$$⊢\left(\neg \forall ww=z\wedge \neg \forall ww=x\right)\to \left(\exists zz=x\to \exists z\exists w\left(z=x\wedge w=y\right)\right)$$
9	1 8	mpi	$$⊢\left(\neg \forall ww=z\wedge \neg \forall ww=x\right)\to \exists z\exists w\left(z=x\wedge w=y\right)$$
10	9	ex	$$⊢\neg \forall ww=z\to \left(\neg \forall ww=x\to \exists z\exists w\left(z=x\wedge w=y\right)\right)$$
11		ax6e	$$⊢\exists zz=y$$
12		nfae	$$⊢Ⅎz\forall ww=x$$
13		equvini	$$⊢z=y\to \exists w\left(z=w\wedge w=y\right)$$
14		equtrr	$$⊢w=x\to \left(z=w\to z=x\right)$$
15	14	anim1d	$$⊢w=x\to \left(\left(z=w\wedge w=y\right)\to \left(z=x\wedge w=y\right)\right)$$
16	15	aleximi	$$⊢\forall ww=x\to \left(\exists w\left(z=w\wedge w=y\right)\to \exists w\left(z=x\wedge w=y\right)\right)$$
17	13 16	syl5	$$⊢\forall ww=x\to \left(z=y\to \exists w\left(z=x\wedge w=y\right)\right)$$
18	12 17	eximd	$$⊢\forall ww=x\to \left(\exists zz=y\to \exists z\exists w\left(z=x\wedge w=y\right)\right)$$
19	11 18	mpi	$$⊢\forall ww=x\to \exists z\exists w\left(z=x\wedge w=y\right)$$
20	10 19	pm2.61d2	$$⊢\neg \forall ww=z\to \exists z\exists w\left(z=x\wedge w=y\right)$$