Theorem rspcdf

Description: Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020)

	Ref	Expression
Hypotheses	rspcdf.1	|- F/ x ph
	rspcdf.2	|- F/ x ch
	rspcdf.3	|- ( ph -> A e. B )
	rspcdf.4	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
Assertion	rspcdf	|- ( ph -> ( A. x e. B ps -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		rspcdf.1	|- F/ x ph
2		rspcdf.2	|- F/ x ch
3		rspcdf.3	|- ( ph -> A e. B )
4		rspcdf.4	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
5	4	ex	|- ( ph -> ( x = A -> ( ps <-> ch ) ) )
6	1 5	alrimi	|- ( ph -> A. x ( x = A -> ( ps <-> ch ) ) )
7	2	rspct	|- ( A. x ( x = A -> ( ps <-> ch ) ) -> ( A e. B -> ( A. x e. B ps -> ch ) ) )
8	6 3 7	sylc	|- ( ph -> ( A. x e. B ps -> ch ) )