Metamath Proof Explorer

Theorem oveqrspc2v

Description: Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014)

Ref Expression
Hypothesis oveqrspc2v.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
Assertion oveqrspc2v ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐹 𝑌 ) = ( 𝑋 𝐺 𝑌 ) )

Proof

Step Hyp Ref Expression
1 oveqrspc2v.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
2 1 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
3 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐹 𝑦 ) = ( 𝑋 𝐹 𝑦 ) )
4 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑦 ) )
5 3 4 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ↔ ( 𝑋 𝐹 𝑦 ) = ( 𝑋 𝐺 𝑦 ) ) )
6 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐹 𝑦 ) = ( 𝑋 𝐹 𝑌 ) )
7 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐺 𝑦 ) = ( 𝑋 𝐺 𝑌 ) )
8 6 7 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 𝐹 𝑦 ) = ( 𝑋 𝐺 𝑦 ) ↔ ( 𝑋 𝐹 𝑌 ) = ( 𝑋 𝐺 𝑌 ) ) )
9 5 8 rspc2v ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐺 𝑦 ) → ( 𝑋 𝐹 𝑌 ) = ( 𝑋 𝐺 𝑌 ) ) )
10 2 9 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 𝐹 𝑌 ) = ( 𝑋 𝐺 𝑌 ) )