Theorem elmapsnd

Description: Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	elmapsnd.1	$$⊢\phi \to FFn\left\{A\right\}$$
	elmapsnd.2	$$⊢\phi \to B\in V$$
	elmapsnd.3	$$⊢\phi \to F\left(A\right)\in B$$
Assertion	elmapsnd	$$⊢\phi \to F\in \left(B^{\left\{A\right\}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmapsnd.1	$$⊢\phi \to FFn\left\{A\right\}$$
2		elmapsnd.2	$$⊢\phi \to B\in V$$
3		elmapsnd.3	$$⊢\phi \to F\left(A\right)\in B$$
4		elsni	$$⊢x\in \left\{A\right\}\to x=A$$
5	4	fveq2d	$$⊢x\in \left\{A\right\}\to F\left(x\right)=F\left(A\right)$$
6	5	adantl	$$⊢\left(\phi \wedge x\in \left\{A\right\}\right)\to F\left(x\right)=F\left(A\right)$$
7	3	adantr	$$⊢\left(\phi \wedge x\in \left\{A\right\}\right)\to F\left(A\right)\in B$$
8	6 7	eqeltrd	$$⊢\left(\phi \wedge x\in \left\{A\right\}\right)\to F\left(x\right)\in B$$
9	8	ralrimiva	$$⊢\phi \to \forall x\in \left\{A\right\}F\left(x\right)\in B$$
10	1 9	jca	$$⊢\phi \to \left(FFn\left\{A\right\}\wedge \forall x\in \left\{A\right\}F\left(x\right)\in B\right)$$
11		ffnfv	$$⊢F:\left\{A\right\}⟶B\leftrightarrow \left(FFn\left\{A\right\}\wedge \forall x\in \left\{A\right\}F\left(x\right)\in B\right)$$
12	10 11	sylibr	$$⊢\phi \to F:\left\{A\right\}⟶B$$
13		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to \left\{A\right\}\in \mathrm{V}$$
15	2 14	elmapd	$$⊢\phi \to \left(F\in \left(B^{\left\{A\right\}}\right)\leftrightarrow F:\left\{A\right\}⟶B\right)$$
16	12 15	mpbird	$$⊢\phi \to F\in \left(B^{\left\{A\right\}}\right)$$