snelmap

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

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

Metamath Proof Explorer