This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) → 𝜓 ) )