Theorem fvmptdv

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

	Ref	Expression
Hypotheses	fvmptd2f.1	|- ( ph -> A e. D )
	fvmptd2f.2	|- ( ( ph /\ x = A ) -> B e. V )
	fvmptd2f.3	|- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )
Assertion	fvmptdv	|- ( ph -> ( F = ( x e. D |-> B ) -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptd2f.1	|- ( ph -> A e. D )
2		fvmptd2f.2	|- ( ( ph /\ x = A ) -> B e. V )
3		fvmptd2f.3	|- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) )
4		nfcv	|- F/_ x F
5		nfv	|- F/ x ps
6	1 2 3 4 5	fvmptd2f	|- ( ph -> ( F = ( x e. D |-> B ) -> ps ) )