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

Metamath Proof Explorer

Theorem mapvalg

Description: The value of set exponentiation. ( A ^m B ) is the set of all functions that map from B to A . Definition 10.24 of Kunen p. 24. (Contributed by NM, 8-Dec-2003) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion mapvalg ⊢ A ∈ C ∧ B ∈ D → A B = f | f : B ⟶ A

Proof

Step Hyp Ref Expression
1 mapex ⊢ B ∈ D ∧ A ∈ C → f | f : B ⟶ A ∈ V
2 1 ancoms ⊢ A ∈ C ∧ B ∈ D → f | f : B ⟶ A ∈ V
3 elex ⊢ A ∈ C → A ∈ V
4 elex ⊢ B ∈ D → B ∈ V
5 feq3 ⊢ x = A → f : y ⟶ x ↔ f : y ⟶ A
6 5 abbidv ⊢ x = A → f | f : y ⟶ x = f | f : y ⟶ A
7 feq2 ⊢ y = B → f : y ⟶ A ↔ f : B ⟶ A
8 7 abbidv ⊢ y = B → f | f : y ⟶ A = f | f : B ⟶ A
9 df-map ⊢ ↑ 𝑚 = x ∈ V , y ∈ V ⟼ f | f : y ⟶ x
10 6 8 9 ovmpog ⊢ A ∈ V ∧ B ∈ V ∧ f | f : B ⟶ A ∈ V → A B = f | f : B ⟶ A
11 10 3expia ⊢ A ∈ V ∧ B ∈ V → f | f : B ⟶ A ∈ V → A B = f | f : B ⟶ A
12 3 4 11 syl2an ⊢ A ∈ C ∧ B ∈ D → f | f : B ⟶ A ∈ V → A B = f | f : B ⟶ A
13 2 12 mpd ⊢ A ∈ C ∧ B ∈ D → A B = f | f : B ⟶ A