# Metamath Proof Explorer

## Theorem f1ssres

Description: A function that is one-to-one is also one-to-one on any subclass of its domain. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Assertion f1ssres ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}\underset{1-1}{⟶}{B}$

### Proof

Step Hyp Ref Expression
1 f1f ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to {F}:{A}⟶{B}$
2 fssres ${⊢}\left({F}:{A}⟶{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}⟶{B}$
3 1 2 sylan ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}⟶{B}$
4 df-f1 ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
5 funres11 ${⊢}\mathrm{Fun}{{F}}^{-1}\to \mathrm{Fun}{\left({{F}↾}_{{C}}\right)}^{-1}$
6 4 5 simplbiim ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to \mathrm{Fun}{\left({{F}↾}_{{C}}\right)}^{-1}$
7 6 adantr ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \mathrm{Fun}{\left({{F}↾}_{{C}}\right)}^{-1}$
8 df-f1 ${⊢}\left({{F}↾}_{{C}}\right):{C}\underset{1-1}{⟶}{B}↔\left(\left({{F}↾}_{{C}}\right):{C}⟶{B}\wedge \mathrm{Fun}{\left({{F}↾}_{{C}}\right)}^{-1}\right)$
9 3 7 8 sylanbrc ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}\underset{1-1}{⟶}{B}$