Theorem mapval

Description: The value of set exponentiation (inference version). ( 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)

	Ref	Expression
Hypotheses	mapval.1	|- A e. _V
	mapval.2	|- B e. _V
Assertion	mapval	|- ( A ^m B ) = { f | f : B --> A }

Proof

Step	Hyp	Ref	Expression
1		mapval.1	|- A e. _V
2		mapval.2	|- B e. _V
3		mapvalg	|- ( ( A e. _V /\ B e. _V ) -> ( A ^m B ) = { f | f : B --> A } )
4	1 2 3	mp2an	|- ( A ^m B ) = { f | f : B --> A }