Theorem ovmpordx

Description: Value of an operation given by a maps-to rule, deduction form, with substitution of second argument, analogous to ovmpodxf . (Contributed by AV, 30-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		ovmpordx.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) )
2		ovmpordx.2	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 = 𝑆 )
3		ovmpordx.3	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐿 )
4		ovmpordx.4	⊢ ( 𝜑 → 𝐴 ∈ 𝐿 )
5		ovmpordx.5	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
6		ovmpordx.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	ovmpordxf	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = 𝑆 )