This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ φ ∧ C ∈ B → F ⁡ C ∈ A
10 5 4 9 syl2anc ⊢ φ → F ⁡ C ∈ A