Metamath Proof Explorer


Theorem f1ssf1

Description: A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020)

Ref Expression
Assertion f1ssf1 FunFFunF-1GFFunG-1

Proof

Step Hyp Ref Expression
1 funssres FunFGFFdomG=G
2 funres11 FunF-1FunFdomG-1
3 cnveq G=FdomGG-1=FdomG-1
4 3 funeqd G=FdomGFunG-1FunFdomG-1
5 2 4 syl5ibr G=FdomGFunF-1FunG-1
6 5 eqcoms FdomG=GFunF-1FunG-1
7 1 6 syl FunFGFFunF-1FunG-1
8 7 ex FunFGFFunF-1FunG-1
9 8 com23 FunFFunF-1GFFunG-1
10 9 3imp FunFFunF-1GFFunG-1