Theorem ovmpodv

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

	Ref	Expression
Hypotheses	ovmpodf.1	$$⊢\phi \to A\in C$$
	ovmpodf.2	$$⊢\left(\phi \wedge x=A\right)\to B\in D$$
	ovmpodf.3	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R\in V$$
	ovmpodf.4	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(AFB=R\to \psi \right)$$
Assertion	ovmpodv	$$⊢\phi \to \left(F=\left(x\in C,y\in D⟼R\right)\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ovmpodf.1	$$⊢\phi \to A\in C$$
2		ovmpodf.2	$$⊢\left(\phi \wedge x=A\right)\to B\in D$$
3		ovmpodf.3	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to R\in V$$
4		ovmpodf.4	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(AFB=R\to \psi \right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xF$$
6		nfv	$$⊢Ⅎx\psi$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}yF$$
8		nfv	$$⊢Ⅎy\psi$$
9	1 2 3 4 5 6 7 8	ovmpodf	$$⊢\phi \to \left(F=\left(x\in C,y\in D⟼R\right)\to \psi \right)$$