Theorem mapsn

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Proof shortened by AV, 17-Jul-2022)

	Ref	Expression
Hypotheses	map0.1	|- A e. _V
	map0.2	|- B e. _V
Assertion	mapsn	|- ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } }

Proof

Step	Hyp	Ref	Expression
1		map0.1	|- A e. _V
2		map0.2	|- B e. _V
3		id	|- ( A e. _V -> A e. _V )
4	2	a1i	|- ( A e. _V -> B e. _V )
5	3 4	mapsnd	|- ( A e. _V -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )
6	1 5	ax-mp	|- ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } }