Metamath Proof Explorer


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 V

Proof

Step Hyp Ref Expression
1 fosetex f | f : A onto B V
2 f1ofo f : A 1-1 onto B f : A onto B
3 2 ss2abi f | f : A 1-1 onto B f | f : A onto B
4 1 3 ssexi f | f : A 1-1 onto B V