Theorem rspc2v

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999)

	Ref	Expression
Hypotheses	rspc2v.1	|- ( x = A -> ( ph <-> ch ) )
	rspc2v.2	|- ( y = B -> ( ch <-> ps ) )
Assertion	rspc2v	|- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		rspc2v.1	|- ( x = A -> ( ph <-> ch ) )
2		rspc2v.2	|- ( y = B -> ( ch <-> ps ) )
3	1	ralbidv	|- ( x = A -> ( A. y e. D ph <-> A. y e. D ch ) )
4	3	rspcv	|- ( A e. C -> ( A. x e. C A. y e. D ph -> A. y e. D ch ) )
5	2	rspcv	|- ( B e. D -> ( A. y e. D ch -> ps ) )
6	4 5	sylan9	|- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph -> ps ) )