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	$$⊢\left\{f|f:A⟶B\right\}\subseteq 𝒫\left(A\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fssxp	$$⊢g:A⟶B\to g\subseteq A\times B$$
2		vex	$$⊢g\in \mathrm{V}$$
3		feq1	$$⊢f=g\to \left(f:A⟶B\leftrightarrow g:A⟶B\right)$$
4	2 3	elab	$$⊢g\in \left\{f|f:A⟶B\right\}\leftrightarrow g:A⟶B$$
5		velpw	$$⊢g\in 𝒫\left(A\times B\right)\leftrightarrow g\subseteq A\times B$$
6	1 4 5	3imtr4i	$$⊢g\in \left\{f|f:A⟶B\right\}\to g\in 𝒫\left(A\times B\right)$$
7	6	ssriv	$$⊢\left\{f|f:A⟶B\right\}\subseteq 𝒫\left(A\times B\right)$$