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