Theorem fvmptdv

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

	Ref	Expression
Hypotheses	fvmptd2f.1	$$⊢\phi \to A\in D$$
	fvmptd2f.2	$$⊢\left(\phi \wedge x=A\right)\to B\in V$$
	fvmptd2f.3	$$⊢\left(\phi \wedge x=A\right)\to \left(F\left(A\right)=B\to \psi \right)$$
Assertion	fvmptdv	$$⊢\phi \to \left(F=\left(x\in D⟼B\right)\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		fvmptd2f.1	$$⊢\phi \to A\in D$$
2		fvmptd2f.2	$$⊢\left(\phi \wedge x=A\right)\to B\in V$$
3		fvmptd2f.3	$$⊢\left(\phi \wedge x=A\right)\to \left(F\left(A\right)=B\to \psi \right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xF$$
5		nfv	$$⊢Ⅎx\psi$$
6	1 2 3 4 5	fvmptd2f	$$⊢\phi \to \left(F=\left(x\in D⟼B\right)\to \psi \right)$$