Theorem snelmap

Description: Membership of the element in the range of a constant map. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	snelmap.a	$$⊢\phi \to A\in V$$
	snelmap.b	$$⊢\phi \to B\in W$$
	snelmap.n	$$⊢\phi \to A\ne \varnothing$$
	snelmap.e	$$⊢\phi \to A\times \left\{x\right\}\in \left(B^A\right)$$
Assertion	snelmap	$$⊢\phi \to x\in B$$

Proof

Step	Hyp	Ref	Expression
1		snelmap.a	$$⊢\phi \to A\in V$$
2		snelmap.b	$$⊢\phi \to B\in W$$
3		snelmap.n	$$⊢\phi \to A\ne \varnothing$$
4		snelmap.e	$$⊢\phi \to A\times \left\{x\right\}\in \left(B^A\right)$$
5		n0	$$⊢A\ne \varnothing \leftrightarrow \exists yy\in A$$
6	3 5	sylib	$$⊢\phi \to \exists yy\in A$$
7		vex	$$⊢x\in \mathrm{V}$$
8	7	fvconst2	$$⊢y\in A\to \left(A\times \left\{x\right\}\right)\left(y\right)=x$$
9	8	eqcomd	$$⊢y\in A\to x=\left(A\times \left\{x\right\}\right)\left(y\right)$$
10	9	adantl	$$⊢\left(\phi \wedge y\in A\right)\to x=\left(A\times \left\{x\right\}\right)\left(y\right)$$
11		elmapg	$$⊢\left(B\in W\wedge A\in V\right)\to \left(A\times \left\{x\right\}\in \left(B^A\right)\leftrightarrow \left(A\times \left\{x\right\}\right):A⟶B\right)$$
12	2 1 11	syl2anc	$$⊢\phi \to \left(A\times \left\{x\right\}\in \left(B^A\right)\leftrightarrow \left(A\times \left\{x\right\}\right):A⟶B\right)$$
13	4 12	mpbid	$$⊢\phi \to \left(A\times \left\{x\right\}\right):A⟶B$$
14	13	adantr	$$⊢\left(\phi \wedge y\in A\right)\to \left(A\times \left\{x\right\}\right):A⟶B$$
15		simpr	$$⊢\left(\phi \wedge y\in A\right)\to y\in A$$
16	14 15	ffvelcdmd	$$⊢\left(\phi \wedge y\in A\right)\to \left(A\times \left\{x\right\}\right)\left(y\right)\in B$$
17	10 16	eqeltrd	$$⊢\left(\phi \wedge y\in A\right)\to x\in B$$
18	17	ex	$$⊢\phi \to \left(y\in A\to x\in B\right)$$
19	18	exlimdv	$$⊢\phi \to \left(\exists yy\in A\to x\in B\right)$$
20	6 19	mpd	$$⊢\phi \to x\in B$$