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	|- ( ( 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		eqidd	|- ( x = C -> F = F )
2		id	|- ( x = C -> x = C )
3		eqidd	|- ( x = C -> y = y )
4	1 2 3	aoveq123d	|- ( x = C -> (( x F y )) = (( C F y )) )
5	4	eqeq2d	|- ( x = C -> ( S = (( x F y )) <-> S = (( C F y )) ) )
6		eqidd	|- ( y = D -> F = F )
7		eqidd	|- ( y = D -> C = C )
8		id	|- ( y = D -> y = D )
9	6 7 8	aoveq123d	|- ( y = D -> (( C F y )) = (( C F D )) )
10	9	eqeq2d	|- ( y = D -> ( S = (( C F y )) <-> S = (( C F D )) ) )
11	5 10	rspc2ev	|- ( ( C e. A /\ D e. B /\ S = (( C F D )) ) -> E. x e. A E. y e. B S = (( x F y )) )