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	|- ( ph -> A e. V )
	elmaprdOLD.2	|- ( ph -> B e. W )
	elmaprdOLD.3	|- ( ph -> F e. ( B ^m A ) )
Assertion	elmaprdOLD	|- ( ph -> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		elmaprdOLD.1	|- ( ph -> A e. V )
2		elmaprdOLD.2	|- ( ph -> B e. W )
3		elmaprdOLD.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 )