Theorem elmaprdOLD

Description: Obsolete version of elmaprd as of 30-Aug-2026. (Contributed by Thierry Arnoux, 13-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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