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