Description: Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fvmap.a | ||
fvmap.b | |||
fvmap.f | |||
fvmap.c | |||
Assertion | fvmap |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmap.a | ||
2 | fvmap.b | ||
3 | fvmap.f | ||
4 | fvmap.c | ||
5 | id | ||
6 | elmapg | ||
7 | 1 2 6 | syl2anc | |
8 | 3 7 | mpbid | |
9 | 8 | ffvelrnda | |
10 | 5 4 9 | syl2anc |