Theorem elmapdd

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

	Ref	Expression
Hypotheses	elmapdd.a	$$⊢\phi \to A\in V$$
	elmapdd.b	$$⊢\phi \to B\in W$$
	elmapdd.c	$$⊢\phi \to C:B⟶A$$
Assertion	elmapdd	$$⊢\phi \to C\in \left(A^B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmapdd.a	$$⊢\phi \to A\in V$$
2		elmapdd.b	$$⊢\phi \to B\in W$$
3		elmapdd.c	$$⊢\phi \to C:B⟶A$$
4	1 2	elmapd	$$⊢\phi \to \left(C\in \left(A^B\right)\leftrightarrow C:B⟶A\right)$$
5	3 4	mpbird	$$⊢\phi \to C\in \left(A^B\right)$$