Theorem spcgv

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of Quine p. 44. (Contributed by NM, 22-Jun-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	spcgv	$$⊢A\in V\to \left(\forall x\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spcgv.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		elex	$$⊢A\in V\to A\in \mathrm{V}$$
3		elex	$$⊢A\in \mathrm{V}\to A\in \mathrm{V}$$
4	1	adantl	$$⊢\left(A\in \mathrm{V}\wedge x=A\right)\to \left(\phi \leftrightarrow \psi \right)$$
5	3 4	spcdv	$$⊢A\in \mathrm{V}\to \left(\forall x\phi \to \psi \right)$$
6	2 5	syl	$$⊢A\in V\to \left(\forall x\phi \to \psi \right)$$