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 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 } )