Theorem rspceov

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

	Ref	Expression
Assertion	rspceov	$$⊢\left(C\in A\wedge D\in B\wedge S=CFD\right)\to \exists x\in A\exists y\in BS=xFy$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=C\to xFy=CFy$$
2	1	eqeq2d	$$⊢x=C\to \left(S=xFy\leftrightarrow S=CFy\right)$$
3		oveq2	$$⊢y=D\to CFy=CFD$$
4	3	eqeq2d	$$⊢y=D\to \left(S=CFy\leftrightarrow S=CFD\right)$$
5	2 4	rspc2ev	$$⊢\left(C\in A\wedge D\in B\wedge S=CFD\right)\to \exists x\in A\exists y\in BS=xFy$$