This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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