Metamath Proof Explorer


Theorem rspceov

Description: A frequently used special case of rspc2ev for operation values. (Contributed by NM, 21-Mar-2007)

Ref Expression
Assertion rspceov
|- ( ( C e. A /\ D e. B /\ S = ( C F D ) ) -> E. x e. A E. y e. B S = ( x F y ) )

Proof

Step Hyp Ref Expression
1 oveq1
 |-  ( x = C -> ( x F y ) = ( C F y ) )
2 1 eqeq2d
 |-  ( x = C -> ( S = ( x F y ) <-> S = ( C F y ) ) )
3 oveq2
 |-  ( y = D -> ( C F y ) = ( C F D ) )
4 3 eqeq2d
 |-  ( y = D -> ( S = ( C F y ) <-> S = ( C F D ) ) )
5 2 4 rspc2ev
 |-  ( ( C e. A /\ D e. B /\ S = ( C F D ) ) -> E. x e. A E. y e. B S = ( x F y ) )