Theorem elmap

Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003)

	Ref	Expression
Hypotheses	elmap.1	$$⊢A\in \mathrm{V}$$
	elmap.2	$$⊢B\in \mathrm{V}$$
Assertion	elmap	$$⊢F\in \left(A^B\right)\leftrightarrow F:B⟶A$$

Proof

Step	Hyp	Ref	Expression
1		elmap.1	$$⊢A\in \mathrm{V}$$
2		elmap.2	$$⊢B\in \mathrm{V}$$
3		elmapg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(F\in \left(A^B\right)\leftrightarrow F:B⟶A\right)$$
4	1 2 3	mp2an	$$⊢F\in \left(A^B\right)\leftrightarrow F:B⟶A$$