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	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ 𝒫 ( 𝐴 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fssxp	⊢ ( 𝑔 : 𝐴 ⟶ 𝐵 → 𝑔 ⊆ ( 𝐴 × 𝐵 ) )
2		vex	⊢ 𝑔 ∈ V
3		feq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑔 : 𝐴 ⟶ 𝐵 ) )
4	2 3	elab	⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↔ 𝑔 : 𝐴 ⟶ 𝐵 )
5		velpw	⊢ ( 𝑔 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↔ 𝑔 ⊆ ( 𝐴 × 𝐵 ) )
6	1 4 5	3imtr4i	⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } → 𝑔 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
7	6	ssriv	⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ⊆ 𝒫 ( 𝐴 × 𝐵 )