Metamath Proof Explorer


Theorem ovmpogad

Description: Value of an operation given by a maps-to rule. Deduction form of ovmpoga . (Contributed by SN, 14-Mar-2025)

Ref Expression
Hypotheses ovmpogad.f 𝐹 = ( 𝑥𝐶 , 𝑦𝐷𝑅 )
ovmpogad.s ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
ovmpogad.1 ( 𝜑𝐴𝐶 )
ovmpogad.2 ( 𝜑𝐵𝐷 )
ovmpogad.v ( 𝜑𝑆𝑉 )
Assertion ovmpogad ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 ovmpogad.f 𝐹 = ( 𝑥𝐶 , 𝑦𝐷𝑅 )
2 ovmpogad.s ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → 𝑅 = 𝑆 )
3 ovmpogad.1 ( 𝜑𝐴𝐶 )
4 ovmpogad.2 ( 𝜑𝐵𝐷 )
5 ovmpogad.v ( 𝜑𝑆𝑉 )
6 1 a1i ( 𝜑𝐹 = ( 𝑥𝐶 , 𝑦𝐷𝑅 ) )
7 2 adantl ( ( 𝜑 ∧ ( 𝑥 = 𝐴𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
8 6 7 3 4 5 ovmpod ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )