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 Gino Giotto, 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	syl6ib	⊢ ( ( 𝐵 ∈ 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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝜓 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝜑 ) )