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	$$⊢B\in V\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		mapfset	$$⊢B\in V\to \left\{f|f:A⟶B\right\}=B^A$$
2		ovex	$$⊢B^A\in \mathrm{V}$$
3	1 2	eqeltrdi	$$⊢B\in V\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$