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 e. C /\ B e. D ) -> ( A ^m B ) = { f | f : B --> A } )

Proof

Step	Hyp	Ref	Expression
1		mapex	|- ( ( B e. D /\ A e. C ) -> { f | f : B --> A } e. _V )
2	1	ancoms	|- ( ( A e. C /\ B e. D ) -> { f | f : B --> A } e. _V )
3		elex	|- ( A e. C -> A e. _V )
4		elex	|- ( B e. D -> B e. _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	|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
10	6 8 9	ovmpog	|- ( ( A e. _V /\ B e. _V /\ { f | f : B --> A } e. _V ) -> ( A ^m B ) = { f | f : B --> A } )
11	10	3expia	|- ( ( A e. _V /\ B e. _V ) -> ( { f | f : B --> A } e. _V -> ( A ^m B ) = { f | f : B --> A } ) )
12	3 4 11	syl2an	|- ( ( A e. C /\ B e. D ) -> ( { f | f : B --> A } e. _V -> ( A ^m B ) = { f | f : B --> A } ) )
13	2 12	mpd	|- ( ( A e. C /\ B e. D ) -> ( A ^m B ) = { f | f : B --> A } )