Theorem ovrspc2v

Description: If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014)

	Ref	Expression
Assertion	ovrspc2v	|- ( ( ( X e. A /\ Y e. B ) /\ A. x e. A A. y e. B ( x F y ) e. C ) -> ( X F Y ) e. C )

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( x = X -> ( x F y ) = ( X F y ) )
2	1	eleq1d	|- ( x = X -> ( ( x F y ) e. C <-> ( X F y ) e. C ) )
3		oveq2	|- ( y = Y -> ( X F y ) = ( X F Y ) )
4	3	eleq1d	|- ( y = Y -> ( ( X F y ) e. C <-> ( X F Y ) e. C ) )
5	2 4	rspc2va	|- ( ( ( X e. A /\ Y e. B ) /\ A. x e. A A. y e. B ( x F y ) e. C ) -> ( X F Y ) e. C )