Theorem f1osetex

Description: The set of bijections between two classes exists. (Contributed by AV, 30-Mar-2024) (Revised by AV, 8-Aug-2024) (Proof shortened by SN, 22-Aug-2024)

	Ref	Expression
Assertion	f1osetex	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}B\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fosetex	$$⊢\left\{f|f:A\underset{onto}{⟶}B\right\}\in \mathrm{V}$$
2		f1ofo	$$⊢f:A\underset{1-1\; onto}{⟶}B\to f:A\underset{onto}{⟶}B$$
3	2	ss2abi	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}B\right\}\subseteq \left\{f|f:A\underset{onto}{⟶}B\right\}$$
4	1 3	ssexi	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}B\right\}\in \mathrm{V}$$