Theorem spcimegf

Description: Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	spcimgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	spcimgf.2	$$⊢Ⅎx\psi$$
	spcimegf.3	$$⊢x=A\to \left(\psi \to \phi \right)$$
Assertion	spcimegf	$$⊢A\in V\to \left(\psi \to \exists x\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spcimgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		spcimgf.2	$$⊢Ⅎx\psi$$
3		spcimegf.3	$$⊢x=A\to \left(\psi \to \phi \right)$$
4	2	nfn	$$⊢Ⅎx\neg \psi$$
5	3	con3d	$$⊢x=A\to \left(\neg \phi \to \neg \psi \right)$$
6	1 4 5	spcimgf	$$⊢A\in V\to \left(\forall x\neg \phi \to \neg \psi \right)$$
7	6	con2d	$$⊢A\in V\to \left(\psi \to \neg \forall x\neg \phi \right)$$
8		df-ex	$$⊢\exists x\phi \leftrightarrow \neg \forall x\neg \phi$$
9	7 8	imbitrrdi	$$⊢A\in V\to \left(\psi \to \exists x\phi \right)$$