Theorem rspc2v

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

	Ref	Expression
Hypotheses	rspc2v.1	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
	rspc2v.2	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
Assertion	rspc2v	$$⊢\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		rspc2v.1	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
2		rspc2v.2	$$⊢y=B\to \left(\chi \leftrightarrow \psi \right)$$
3	1	ralbidv	$$⊢x=A\to \left(\forall y\in D\phi \leftrightarrow \forall y\in D\chi \right)$$
4	3	rspcv	$$⊢A\in C\to \left(\forall x\in C\forall y\in D\phi \to \forall y\in D\chi \right)$$
5	2	rspcv	$$⊢B\in D\to \left(\forall y\in D\chi \to \psi \right)$$
6	4 5	sylan9	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\forall x\in C\forall y\in D\phi \to \psi \right)$$