Metamath Proof Explorer


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 φAV
snelmap.b φBW
snelmap.n φA
snelmap.e φA×xBA
Assertion snelmap φxB

Proof

Step Hyp Ref Expression
1 snelmap.a φAV
2 snelmap.b φBW
3 snelmap.n φA
4 snelmap.e φA×xBA
5 n0 AyyA
6 3 5 sylib φyyA
7 vex xV
8 7 fvconst2 yAA×xy=x
9 8 eqcomd yAx=A×xy
10 9 adantl φyAx=A×xy
11 elmapg BWAVA×xBAA×x:AB
12 2 1 11 syl2anc φA×xBAA×x:AB
13 4 12 mpbid φA×x:AB
14 13 adantr φyAA×x:AB
15 simpr φyAyA
16 14 15 ffvelrnd φyAA×xyB
17 10 16 eqeltrd φyAxB
18 17 ex φyAxB
19 18 exlimdv φyyAxB
20 6 19 mpd φxB