Theorem fsetex

Description: The set of functions between two classes exists if the codomain exists. Generalization of mapex to arbitrary domains. (Contributed by AV, 14-Aug-2024)

	Ref	Expression
Assertion	fsetex	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		mapfset	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ( 𝐵 ↑m 𝐴 ) )
2		ovex	⊢ ( 𝐵 ↑m 𝐴 ) ∈ V
3	1 2	eqeltrdi	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )