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