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

Proof

Step	Hyp	Ref	Expression
1		fsetex	$$⊢B\in V\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$
2		df-f1	$$⊢f:A\underset{1-1}{⟶}B\leftrightarrow \left(f:A⟶B\wedge \mathrm{Fun}{f}^{-1}\right)$$
3	2	abbii	$$⊢\left\{f|f:A\underset{1-1}{⟶}B\right\}=\left\{f|\left(f:A⟶B\wedge \mathrm{Fun}{f}^{-1}\right)\right\}$$
4		abanssl	$$⊢\left\{f|\left(f:A⟶B\wedge \mathrm{Fun}{f}^{-1}\right)\right\}\subseteq \left\{f|f:A⟶B\right\}$$
5	3 4	eqsstri	$$⊢\left\{f|f:A\underset{1-1}{⟶}B\right\}\subseteq \left\{f|f:A⟶B\right\}$$
6	5	a1i	$$⊢B\in V\to \left\{f|f:A\underset{1-1}{⟶}B\right\}\subseteq \left\{f|f:A⟶B\right\}$$
7	1 6	ssexd	$$⊢B\in V\to \left\{f|f:A\underset{1-1}{⟶}B\right\}\in \mathrm{V}$$