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

Metamath Proof Explorer

Theorem elmaprd

Description: Deduction associated with elmapd . Reverse direction of elmapdd . (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses elmaprd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
elmaprd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
elmaprd.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) )
Assertion elmaprd ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 elmaprd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 elmaprd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 elmaprd.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) )
4 2 1 elmapd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
5 3 4 mpbid ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )