Theorem fvmptdv

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

	Ref	Expression
Hypotheses	fvmptd2f.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	fvmptd2f.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑉 )
	fvmptd2f.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝜓 ) )
Assertion	fvmptdv	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		fvmptd2f.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
2		fvmptd2f.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑉 )
3		fvmptd2f.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝜓 ) )
4		nfcv	⊢ Ⅎ 𝑥 𝐹
5		nfv	⊢ Ⅎ 𝑥 𝜓
6	1 2 3 4 5	fvmptd2f	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )