Theorem ovmpodv

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

	Ref	Expression
Hypotheses	ovmpodf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
	ovmpodf.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝐷 )
	ovmpodf.3	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 ∈ 𝑉 )
	ovmpodf.4	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝑅 → 𝜓 ) )
Assertion	ovmpodv	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ovmpodf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
2		ovmpodf.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝐷 )
3		ovmpodf.3	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝑅 ∈ 𝑉 )
4		ovmpodf.4	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝐴 𝐹 𝐵 ) = 𝑅 → 𝜓 ) )
5		nfcv	⊢ Ⅎ 𝑥 𝐹
6		nfv	⊢ Ⅎ 𝑥 𝜓
7		nfcv	⊢ Ⅎ 𝑦 𝐹
8		nfv	⊢ Ⅎ 𝑦 𝜓
9	1 2 3 4 5 6 7 8	ovmpodf	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐷 ↦ 𝑅 ) → 𝜓 ) )