Theorem elmaprd

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

	Ref	Expression
Hypotheses	elmaprd.1	|- ( ph -> A e. V )
	elmaprd.2	|- ( ph -> B e. W )
	elmaprd.3	|- ( ph -> F e. ( B ^m A ) )
Assertion	elmaprd	|- ( ph -> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		elmaprd.1	|- ( ph -> A e. V )
2		elmaprd.2	|- ( ph -> B e. W )
3		elmaprd.3	|- ( ph -> F e. ( B ^m A ) )
4	2 1	elmapd	|- ( ph -> ( F e. ( B ^m A ) <-> F : A --> B ) )
5	3 4	mpbid	|- ( ph -> F : A --> B )