Theorem mapssfset

Description: The value of the set exponentiation ( B ^m A ) is a subset of the class of functions from A to B . (Contributed by AV, 10-Aug-2024)

	Ref	Expression
Assertion	mapssfset	|- ( B ^m A ) C_ { f | f : A --> B }

Proof

Step	Hyp	Ref	Expression
1		mapfset	|- ( B e. _V -> { f | f : A --> B } = ( B ^m A ) )
2		eqimss2	|- ( { f | f : A --> B } = ( B ^m A ) -> ( B ^m A ) C_ { f | f : A --> B } )
3	1 2	syl	|- ( B e. _V -> ( B ^m A ) C_ { f | f : A --> B } )
4		reldmmap	|- Rel dom ^m
5	4	ovprc1	|- ( -. B e. _V -> ( B ^m A ) = (/) )
6		0ss	|- (/) C_ { f | f : A --> B }
7	5 6	eqsstrdi	|- ( -. B e. _V -> ( B ^m A ) C_ { f | f : A --> B } )
8	3 7	pm2.61i	|- ( B ^m A ) C_ { f | f : A --> B }