Theorem f1ssr 5792

Description: A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Stefan O'Rear, 20-Feb-2015.)

Assertion

Ref	Expression
f1ssr

Proof of Theorem f1ssr

Step	Hyp	Ref	Expression
1		f1fn 5787	. . . 4
2	1	adantr 465	. . 3
3		simpr 461	. . 3
4		df-f 5597	. . 3
5	2, 3, 4	sylanbrc 664	. 2
6		df-f1 5598	. . . 4
7	6	simprbi 464	. . 3
8	7	adantr 465	. 2
9		df-f1 5598	. 2
10	5, 8, 9	sylanbrc 664	1

Syntax hints:  ->wi 4  /\wa 369  C_wss 3475  `'ccnv 5003  rancrn 5005  Funwfun 5587  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590

This theorem is referenced by:  domdifsn  7620  marypha1  7914  m2cpmf1  19244  usgrares1  24410  usgresvm1  32443  usgresvm1ALT  32447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-f 5597  df-f1 5598