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 w w = z \to \exists z \exists w (z = x \land w = y)$

Proof

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

Metamath Proof Explorer

Theorem 2ax6elem

Proof