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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )