Theorem oveqrspc2v

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

	Ref	Expression
Hypothesis	oveqrspc2v.1	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x F y ) = ( x G y ) )
Assertion	oveqrspc2v	|- ( ( ph /\ ( X e. A /\ Y e. B ) ) -> ( X F Y ) = ( X G Y ) )

Proof

Step	Hyp	Ref	Expression
1		oveqrspc2v.1	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x F y ) = ( x G y ) )
2	1	ralrimivva	|- ( ph -> A. x e. A A. y e. B ( x F y ) = ( x G y ) )
3		oveq1	|- ( x = X -> ( x F y ) = ( X F y ) )
4		oveq1	|- ( x = X -> ( x G y ) = ( X G y ) )
5	3 4	eqeq12d	|- ( x = X -> ( ( x F y ) = ( x G y ) <-> ( X F y ) = ( X G y ) ) )
6		oveq2	|- ( y = Y -> ( X F y ) = ( X F Y ) )
7		oveq2	|- ( y = Y -> ( X G y ) = ( X G Y ) )
8	6 7	eqeq12d	|- ( y = Y -> ( ( X F y ) = ( X G y ) <-> ( X F Y ) = ( X G Y ) ) )
9	5 8	rspc2v	|- ( ( X e. A /\ Y e. B ) -> ( A. x e. A A. y e. B ( x F y ) = ( x G y ) -> ( X F Y ) = ( X G Y ) ) )
10	2 9	mpan9	|- ( ( ph /\ ( X e. A /\ Y e. B ) ) -> ( X F Y ) = ( X G Y ) )