Theorem fvmptd2f

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

	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)$$
	fvmptd2f.4	$$⊢\underset{\_}{Ⅎ}xF$$
	fvmptd2f.5	$$⊢Ⅎx\psi$$
Assertion	fvmptd2f	$$⊢\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		fvmptd2f.4	$$⊢\underset{\_}{Ⅎ}xF$$
5		fvmptd2f.5	$$⊢Ⅎx\psi$$
6		nfv	$$⊢Ⅎx\phi$$
7	1 2 3 4 5 6	fvmptd3f	$$⊢\phi \to \left(F=\left(x\in D⟼B\right)\to \psi \right)$$