Theorem ovmpod

Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	ovmpod.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
	ovmpod.2	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
	ovmpod.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	ovmpod.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	ovmpod.5	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
Assertion	ovmpod	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ovmpod.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
2		ovmpod.2	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
3		ovmpod.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
4		ovmpod.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
5		ovmpod.5	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
6		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐷 = 𝐷 )
7	1 2 6 3 4 5	ovmpodx	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )