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	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spc3egv	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(\psi \to \exists x\exists y\exists z\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spc3egv.1	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		elex	$$⊢A\in V\to A\in \mathrm{V}$$
3		elex	$$⊢B\in W\to B\in \mathrm{V}$$
4		elex	$$⊢C\in X\to C\in \mathrm{V}$$
5		simp1	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to A\in \mathrm{V}$$
6	1	3coml	$$⊢\left(y=B\wedge z=C\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
7	6	3expa	$$⊢\left(\left(y=B\wedge z=C\right)\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
8	7	pm5.74da	$$⊢\left(y=B\wedge z=C\right)\to \left(\left(x=A\to \phi \right)\leftrightarrow \left(x=A\to \psi \right)\right)$$
9	8	spc2egv	$$⊢\left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(\left(x=A\to \psi \right)\to \exists y\exists z\left(x=A\to \phi \right)\right)$$
10		19.37v	$$⊢\exists z\left(x=A\to \phi \right)\leftrightarrow \left(x=A\to \exists z\phi \right)$$
11	10	exbii	$$⊢\exists y\exists z\left(x=A\to \phi \right)\leftrightarrow \exists y\left(x=A\to \exists z\phi \right)$$
12		19.37v	$$⊢\exists y\left(x=A\to \exists z\phi \right)\leftrightarrow \left(x=A\to \exists y\exists z\phi \right)$$
13	11 12	bitri	$$⊢\exists y\exists z\left(x=A\to \phi \right)\leftrightarrow \left(x=A\to \exists y\exists z\phi \right)$$
14	9 13	imbitrdi	$$⊢\left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(\left(x=A\to \psi \right)\to \left(x=A\to \exists y\exists z\phi \right)\right)$$
15	14	pm2.86d	$$⊢\left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(x=A\to \left(\psi \to \exists y\exists z\phi \right)\right)$$
16	15	3adant1	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(x=A\to \left(\psi \to \exists y\exists z\phi \right)\right)$$
17	16	imp	$$⊢\left(\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\wedge x=A\right)\to \left(\psi \to \exists y\exists z\phi \right)$$
18	5 17	spcimedv	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(\psi \to \exists x\exists y\exists z\phi \right)$$
19	2 3 4 18	syl3an	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(\psi \to \exists x\exists y\exists z\phi \right)$$