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	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) → ( 𝑋 𝐹 𝑌 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐹 𝑦 ) = ( 𝑋 𝐹 𝑦 ) )
2	1	eleq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ↔ ( 𝑋 𝐹 𝑦 ) ∈ 𝐶 ) )
3		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐹 𝑦 ) = ( 𝑋 𝐹 𝑌 ) )
4	3	eleq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 𝐹 𝑦 ) ∈ 𝐶 ↔ ( 𝑋 𝐹 𝑌 ) ∈ 𝐶 ) )
5	2 4	rspc2va	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) ∈ 𝐶 ) → ( 𝑋 𝐹 𝑌 ) ∈ 𝐶 )