Theorem spcegv

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

	Ref	Expression
Hypothesis	spcgv.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spcegv	$$⊢A\in V\to \left(\psi \to \exists x\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		elisset	$$⊢A\in V\to \exists xx=A$$
3	1	biimprcd	$$⊢\psi \to \left(x=A\to \phi \right)$$
4	3	eximdv	$$⊢\psi \to \left(\exists xx=A\to \exists x\phi \right)$$
5	2 4	syl5com	$$⊢A\in V\to \left(\psi \to \exists x\phi \right)$$