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	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝐴 )