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	⊢ ( ¬ ∀ 𝑤 𝑤 = 𝑧 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		ax6e	⊢ ∃ 𝑧 𝑧 = 𝑥
2		nfnae	⊢ Ⅎ 𝑧 ¬ ∀ 𝑤 𝑤 = 𝑧
3		nfnae	⊢ Ⅎ 𝑧 ¬ ∀ 𝑤 𝑤 = 𝑥
4	2 3	nfan	⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑤 𝑤 = 𝑧 ∧ ¬ ∀ 𝑤 𝑤 = 𝑥 )
5		nfeqf	⊢ ( ( ¬ ∀ 𝑤 𝑤 = 𝑧 ∧ ¬ ∀ 𝑤 𝑤 = 𝑥 ) → Ⅎ 𝑤 𝑧 = 𝑥 )
6		pm3.21	⊢ ( 𝑤 = 𝑦 → ( 𝑧 = 𝑥 → ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
7	5 6	spimed	⊢ ( ( ¬ ∀ 𝑤 𝑤 = 𝑧 ∧ ¬ ∀ 𝑤 𝑤 = 𝑥 ) → ( 𝑧 = 𝑥 → ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
8	4 7	eximd	⊢ ( ( ¬ ∀ 𝑤 𝑤 = 𝑧 ∧ ¬ ∀ 𝑤 𝑤 = 𝑥 ) → ( ∃ 𝑧 𝑧 = 𝑥 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
9	1 8	mpi	⊢ ( ( ¬ ∀ 𝑤 𝑤 = 𝑧 ∧ ¬ ∀ 𝑤 𝑤 = 𝑥 ) → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
10	9	ex	⊢ ( ¬ ∀ 𝑤 𝑤 = 𝑧 → ( ¬ ∀ 𝑤 𝑤 = 𝑥 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
11		ax6e	⊢ ∃ 𝑧 𝑧 = 𝑦
12		nfae	⊢ Ⅎ 𝑧 ∀ 𝑤 𝑤 = 𝑥
13		equvini	⊢ ( 𝑧 = 𝑦 → ∃ 𝑤 ( 𝑧 = 𝑤 ∧ 𝑤 = 𝑦 ) )
14		equtrr	⊢ ( 𝑤 = 𝑥 → ( 𝑧 = 𝑤 → 𝑧 = 𝑥 ) )
15	14	anim1d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑧 = 𝑤 ∧ 𝑤 = 𝑦 ) → ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
16	15	aleximi	⊢ ( ∀ 𝑤 𝑤 = 𝑥 → ( ∃ 𝑤 ( 𝑧 = 𝑤 ∧ 𝑤 = 𝑦 ) → ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
17	13 16	syl5	⊢ ( ∀ 𝑤 𝑤 = 𝑥 → ( 𝑧 = 𝑦 → ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
18	12 17	eximd	⊢ ( ∀ 𝑤 𝑤 = 𝑥 → ( ∃ 𝑧 𝑧 = 𝑦 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ) )
19	11 18	mpi	⊢ ( ∀ 𝑤 𝑤 = 𝑥 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
20	10 19	pm2.61d2	⊢ ( ¬ ∀ 𝑤 𝑤 = 𝑧 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )