Metamath Proof Explorer


Theorem fvmap

Description: Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses fvmap.a φ A V
fvmap.b φ B W
fvmap.f φ F A B
fvmap.c φ C B
Assertion fvmap φ F C A

Proof

Step Hyp Ref Expression
1 fvmap.a φ A V
2 fvmap.b φ B W
3 fvmap.f φ F A B
4 fvmap.c φ C B
5 id φ φ
6 elmapg A V B W F A B F : B A
7 1 2 6 syl2anc φ F A B F : B A
8 3 7 mpbid φ F : B A
9 8 ffvelrnda φ C B F C A
10 5 4 9 syl2anc φ F C A