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	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )