Metamath Proof Explorer


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 A f | f : A B

Proof

Step Hyp Ref Expression
1 mapfset B V f | f : A B = B A
2 eqimss2 f | f : A B = B A B A f | f : A B
3 1 2 syl B V B A f | f : A B
4 reldmmap Rel dom 𝑚
5 4 ovprc1 ¬ B V B A =
6 0ss f | f : A B
7 5 6 eqsstrdi ¬ B V B A f | f : A B
8 3 7 pm2.61i B A f | f : A B