Theorem spcegf

Description: Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997)

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

Proof

Step	Hyp	Ref	Expression
1		spcgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		spcgf.2	$$⊢Ⅎx\psi$$
3		spcgf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4	2	nfn	$$⊢Ⅎx\neg \psi$$
5	3	notbid	$$⊢x=A\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
6	1 4 5	spcgf	$$⊢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)$$