Theorem rspcdva

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020)

	Ref	Expression
Hypotheses	rspcdva.1	$$⊢x=C\to \left(\psi \leftrightarrow \chi \right)$$
	rspcdva.2	$$⊢\phi \to \forall x\in A\psi$$
	rspcdva.3	$$⊢\phi \to C\in A$$
Assertion	rspcdva	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		rspcdva.1	$$⊢x=C\to \left(\psi \leftrightarrow \chi \right)$$
2		rspcdva.2	$$⊢\phi \to \forall x\in A\psi$$
3		rspcdva.3	$$⊢\phi \to C\in A$$
4	1	rspcv	$$⊢C\in A\to \left(\forall x\in A\psi \to \chi \right)$$
5	3 2 4	sylc	$$⊢\phi \to \chi$$