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

Metamath Proof Explorer

Theorem spc3egv

Description: Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023) (Proof shortened by Wolf Lammen, 25-Aug-2023)

Ref Expression
Hypothesis spc3egv.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion spc3egv ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝜓 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝜑 ) )

Proof

Step Hyp Ref Expression
1 spc3egv.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
2 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3 elex ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
4 elex ⊢ ( 𝐶 ∈ 𝑋 → 𝐶 ∈ V )
5 simp1 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → 𝐴 ∈ V )
6 1 3coml ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝑥 = 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
7 6 3expa ⊢ ( ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝑥 = 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
8 7 pm5.74da ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜓 ) ) )
9 8 spc2egv ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝑥 = 𝐴 → 𝜓 ) → ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 → 𝜑 ) ) )
10 19.37v ⊢ ( ∃ 𝑧 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → ∃ 𝑧 𝜑 ) )
11 10 exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 = 𝐴 → ∃ 𝑧 𝜑 ) )
12 19.37v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 → ∃ 𝑧 𝜑 ) ↔ ( 𝑥 = 𝐴 → ∃ 𝑦 ∃ 𝑧 𝜑 ) )
13 11 12 bitri ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → ∃ 𝑦 ∃ 𝑧 𝜑 ) )
14 9 13 imbitrdi ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( ( 𝑥 = 𝐴 → 𝜓 ) → ( 𝑥 = 𝐴 → ∃ 𝑦 ∃ 𝑧 𝜑 ) ) )
15 14 pm2.86d ⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝑥 = 𝐴 → ( 𝜓 → ∃ 𝑦 ∃ 𝑧 𝜑 ) ) )
16 15 3adant1 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝑥 = 𝐴 → ( 𝜓 → ∃ 𝑦 ∃ 𝑧 𝜑 ) ) )
17 16 imp ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ 𝑥 = 𝐴 ) → ( 𝜓 → ∃ 𝑦 ∃ 𝑧 𝜑 ) )
18 5 17 spcimedv ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝜓 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝜑 ) )
19 2 3 4 18 syl3an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝜓 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝜑 ) )