This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funres11

Description: The restriction of a one-to-one function is one-to-one. (Contributed by NM, 25-Mar-1998)

Ref Expression
Assertion funres11 ⊢ Fun ⁡ F -1 → Fun ⁡ F ↾ A -1

Proof

Step Hyp Ref Expression
1 resss ⊢ F ↾ A ⊆ F
2 cnvss ⊢ F ↾ A ⊆ F → F ↾ A -1 ⊆ F -1
3 funss ⊢ F ↾ A -1 ⊆ F -1 → Fun ⁡ F -1 → Fun ⁡ F ↾ A -1
4 1 2 3 mp2b ⊢ Fun ⁡ F -1 → Fun ⁡ F ↾ A -1