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

Proof

Step	Hyp	Ref	Expression
1		fosetex	|- { f | f : A -onto-> B } e. _V
2		f1ofo	|- ( f : A -1-1-onto-> B -> f : A -onto-> B )
3	2	ss2abi	|- { f | f : A -1-1-onto-> B } C_ { f | f : A -onto-> B }
4	1 3	ssexi	|- { f | f : A -1-1-onto-> B } e. _V