Theorem rspc2

Description: Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		rspc2.1	|- F/ x ch
2		rspc2.2	|- F/ y ps
3		rspc2.3	|- ( x = A -> ( ph <-> ch ) )
4		rspc2.4	|- ( y = B -> ( ch <-> ps ) )
5		nfcv	|- F/_ x D
6	5 1	nfralw	|- F/ x A. y e. D ch
7	3	ralbidv	|- ( x = A -> ( A. y e. D ph <-> A. y e. D ch ) )
8	6 7	rspc	|- ( A e. C -> ( A. x e. C A. y e. D ph -> A. y e. D ch ) )
9	2 4	rspc	|- ( B e. D -> ( A. y e. D ch -> ps ) )
10	8 9	sylan9	|- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph -> ps ) )