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	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	fvmptd2f.2	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑉 )
	fvmptd2f.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝐹 ‘ 𝐴 ) = 𝐵 → 𝜓 ) )
	fvmptd2f.4	⊢ Ⅎ 𝑥 𝐹
	fvmptd2f.5	⊢ Ⅎ 𝑥 𝜓
Assertion	fvmptd2f	⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )

Proof

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