Theorem ovmpodx

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

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

Proof

Step	Hyp	Ref	Expression
1		ovmpodx.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
2		ovmpodx.2	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
3		ovmpodx.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐷 = 𝐿 )
4		ovmpodx.4	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
5		ovmpodx.5	⊢ ( 𝜑 → 𝐵 ∈ 𝐿 )
6		ovmpodx.6	⊢ ( 𝜑 → 𝑆 ∈ 𝑋 )
7		nfv	⊢ Ⅎ 𝑥 𝜑
8		nfv	⊢ Ⅎ 𝑦 𝜑
9		nfcv	⊢ Ⅎ 𝑦 𝐴
10		nfcv	⊢ Ⅎ 𝑥 𝐵
11		nfcv	⊢ Ⅎ 𝑥 𝑆
12		nfcv	⊢ Ⅎ 𝑦 𝑆
13	1 2 3 4 5 6 7 8 9 10 11 12	ovmpodxf	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )