Theorem rspcdva

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

	Ref	Expression
Hypotheses	rspcdva.1	|- ( x = C -> ( ps <-> ch ) )
	rspcdva.2	|- ( ph -> A. x e. A ps )
	rspcdva.3	|- ( ph -> C e. A )
Assertion	rspcdva	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		rspcdva.1	|- ( x = C -> ( ps <-> ch ) )
2		rspcdva.2	|- ( ph -> A. x e. A ps )
3		rspcdva.3	|- ( ph -> C e. A )
4	1	rspcv	|- ( C e. A -> ( A. x e. A ps -> ch ) )
5	3 2 4	sylc	|- ( ph -> ch )