Theorem rspceaov

Description: A frequently used special case of rspc2ev for operation values, analogous to rspceov . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	rspceaov	$$⊢\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		eqidd	$$⊢x=C\to F=F$$
2		id	$$⊢x=C\to x=C$$
3		eqidd	$$⊢x=C\to y=y$$
4	1 2 3	aoveq123d	$$⊢x=C\to ((xFy))=((CFy))$$
5	4	eqeq2d	$$⊢x=C\to \left(S=((xFy))\leftrightarrow S=((CFy))\right)$$
6		eqidd	$$⊢y=D\to F=F$$
7		eqidd	$$⊢y=D\to C=C$$
8		id	$$⊢y=D\to y=D$$
9	6 7 8	aoveq123d	$$⊢y=D\to ((CFy))=((CFD))$$
10	9	eqeq2d	$$⊢y=D\to \left(S=((CFy))\leftrightarrow S=((CFD))\right)$$
11	5 10	rspc2ev	$$⊢\left(C\in A\wedge D\in B\wedge S=((CFD))\right)\to \exists x\in A\exists y\in BS=((xFy))$$