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 ( 𝜑𝐴𝑉 )
fvmap.b ( 𝜑𝐵𝑊 )
fvmap.f ( 𝜑𝐹 ∈ ( 𝐴m 𝐵 ) )
fvmap.c ( 𝜑𝐶𝐵 )
Assertion fvmap ( 𝜑 → ( 𝐹𝐶 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 fvmap.a ( 𝜑𝐴𝑉 )
2 fvmap.b ( 𝜑𝐵𝑊 )
3 fvmap.f ( 𝜑𝐹 ∈ ( 𝐴m 𝐵 ) )
4 fvmap.c ( 𝜑𝐶𝐵 )
5 id ( 𝜑𝜑 )
6 elmapg ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐹 ∈ ( 𝐴m 𝐵 ) ↔ 𝐹 : 𝐵𝐴 ) )
7 1 2 6 syl2anc ( 𝜑 → ( 𝐹 ∈ ( 𝐴m 𝐵 ) ↔ 𝐹 : 𝐵𝐴 ) )
8 3 7 mpbid ( 𝜑𝐹 : 𝐵𝐴 )
9 8 ffvelrnda ( ( 𝜑𝐶𝐵 ) → ( 𝐹𝐶 ) ∈ 𝐴 )
10 5 4 9 syl2anc ( 𝜑 → ( 𝐹𝐶 ) ∈ 𝐴 )