Theorem oveqrspc2v

Description: Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014)

	Ref	Expression
Hypothesis	oveqrspc2v.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to xFy=xGy$$
Assertion	oveqrspc2v	$$⊢\left(\phi \wedge \left(X\in A\wedge Y\in B\right)\right)\to XFY=XGY$$

Proof

Step	Hyp	Ref	Expression
1		oveqrspc2v.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to xFy=xGy$$
2	1	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in BxFy=xGy$$
3		oveq1	$$⊢x=X\to xFy=XFy$$
4		oveq1	$$⊢x=X\to xGy=XGy$$
5	3 4	eqeq12d	$$⊢x=X\to \left(xFy=xGy\leftrightarrow XFy=XGy\right)$$
6		oveq2	$$⊢y=Y\to XFy=XFY$$
7		oveq2	$$⊢y=Y\to XGy=XGY$$
8	6 7	eqeq12d	$$⊢y=Y\to \left(XFy=XGy\leftrightarrow XFY=XGY\right)$$
9	5 8	rspc2v	$$⊢\left(X\in A\wedge Y\in B\right)\to \left(\forall x\in A\forall y\in BxFy=xGy\to XFY=XGY\right)$$
10	2 9	mpan9	$$⊢\left(\phi \wedge \left(X\in A\wedge Y\in B\right)\right)\to XFY=XGY$$