Theorem spcev

Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993) (Proof shortened by Eric Schmidt, 22-Dec-2006)

	Ref	Expression
Hypotheses	spcv.1	$$⊢A\in \mathrm{V}$$
	spcv.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spcev	$$⊢\psi \to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		spcv.1	$$⊢A\in \mathrm{V}$$
2		spcv.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3	2	spcegv	$$⊢A\in \mathrm{V}\to \left(\psi \to \exists x\phi \right)$$
4	1 3	ax-mp	$$⊢\psi \to \exists x\phi$$