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

Metamath Proof Explorer

Theorem feqmptd

Description: Deduction form of dffn5 . (Contributed by Mario Carneiro, 8-Jan-2015)

Ref Expression
Hypothesis feqmptd.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion feqmptd ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 feqmptd.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3 dffn5 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
4 2 3 sylib ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )