Theorem f1setex

Description: The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024)

	Ref	Expression
Assertion	f1setex	|- ( B e. V -> { f | f : A -1-1-> B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		fsetex	|- ( B e. V -> { f | f : A --> B } e. _V )
2		df-f1	|- ( f : A -1-1-> B <-> ( f : A --> B /\ Fun `' f ) )
3	2	abbii	|- { f | f : A -1-1-> B } = { f | ( f : A --> B /\ Fun `' f ) }
4		abanssl	|- { f | ( f : A --> B /\ Fun `' f ) } C_ { f | f : A --> B }
5	3 4	eqsstri	|- { f | f : A -1-1-> B } C_ { f | f : A --> B }
6	5	a1i	|- ( B e. V -> { f | f : A -1-1-> B } C_ { f | f : A --> B } )
7	1 6	ssexd	|- ( B e. V -> { f | f : A -1-1-> B } e. _V )