Metamath Proof Explorer


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 V f | f : A 1-1 B V

Proof

Step Hyp Ref Expression
1 fsetex B V f | f : A B V
2 df-f1 f : A 1-1 B f : A B Fun f -1
3 2 abbii f | f : A 1-1 B = f | f : A B Fun f -1
4 abanssl f | f : A B Fun f -1 f | f : A B
5 3 4 eqsstri f | f : A 1-1 B f | f : A B
6 5 a1i B V f | f : A 1-1 B f | f : A B
7 1 6 ssexd B V f | f : A 1-1 B V