This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )