Metamath Proof Explorer

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 \in A \land Y \in B) \land \forall x \in A \forall y \in B x F y \in C) \to X F Y \in C$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = X \to x F y = X F y$
2	1	eleq1d	$⊢ x = X \to (x F y \in C \leftrightarrow X F y \in C)$
3		oveq2	$⊢ y = Y \to X F y = X F Y$
4	3	eleq1d	$⊢ y = Y \to (X F y \in C \leftrightarrow X F Y \in C)$
5	2 4	rspc2va	$⊢ ((X \in A \land Y \in B) \land \forall x \in A \forall y \in B x F y \in C) \to X F Y \in C$