Theorem rspc2

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

	Ref	Expression
Hypotheses	rspc2.1	$$⊢Ⅎx\chi$$
	rspc2.2	$$⊢Ⅎy\psi$$
	rspc2.3	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
	rspc2.4	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	rspc2	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\forall x\in C\forall y\in D\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rspc2.1	$$⊢Ⅎx\chi$$
2		rspc2.2	$$⊢Ⅎy\psi$$
3		rspc2.3	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
4		rspc2.4	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
6	5 1	nfralw	$$⊢Ⅎx\forall y\in D\chi$$
7	3	ralbidv	$$⊢x=A\to \left(\forall y\in D\phi \leftrightarrow \forall y\in D\chi \right)$$
8	6 7	rspc	$$⊢A\in C\to \left(\forall x\in C\forall y\in D\phi \to \forall y\in D\chi \right)$$
9	2 4	rspc	$$⊢B\in D\to \left(\forall y\in D\chi \to \psi \right)$$
10	8 9	sylan9	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\forall x\in C\forall y\in D\phi \to \psi \right)$$