Theorem elmapdd

Description: Deduction associated with elmapd . (Contributed by SN, 29-Jul-2024)

	Ref	Expression
Hypotheses	elmapdd.a	|- ( ph -> A e. V )
	elmapdd.b	|- ( ph -> B e. W )
	elmapdd.c	|- ( ph -> C : B --> A )
Assertion	elmapdd	|- ( ph -> C e. ( A ^m B ) )

Proof

Step	Hyp	Ref	Expression
1		elmapdd.a	|- ( ph -> A e. V )
2		elmapdd.b	|- ( ph -> B e. W )
3		elmapdd.c	|- ( ph -> C : B --> A )
4	1 2	elmapd	|- ( ph -> ( C e. ( A ^m B ) <-> C : B --> A ) )
5	3 4	mpbird	|- ( ph -> C e. ( A ^m B ) )