Theorem fsetsspwxp

Description: The class of all functions from A into B is a subclass of the power class of the cartesion product of A and B . (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Assertion	fsetsspwxp	|- { f | f : A --> B } C_ ~P ( A X. B )

Proof

Step	Hyp	Ref	Expression
1		fssxp	|- ( g : A --> B -> g C_ ( A X. B ) )
2		vex	|- g e. _V
3		feq1	|- ( f = g -> ( f : A --> B <-> g : A --> B ) )
4	2 3	elab	|- ( g e. { f | f : A --> B } <-> g : A --> B )
5		velpw	|- ( g e. ~P ( A X. B ) <-> g C_ ( A X. B ) )
6	1 4 5	3imtr4i	|- ( g e. { f | f : A --> B } -> g e. ~P ( A X. B ) )
7	6	ssriv	|- { f | f : A --> B } C_ ~P ( A X. B )