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 e. V -> { f | f : A --> B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		mapfset	|- ( B e. V -> { f | f : A --> B } = ( B ^m A ) )
2		ovex	|- ( B ^m A ) e. _V
3	1 2	eqeltrdi	|- ( B e. V -> { f | f : A --> B } e. _V )