Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1ss | Structured version Visualization version Unicode version |
Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013.) |
Ref | Expression |
---|---|
f1ss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1f 6101 | . . 3 | |
2 | fss 6056 | . . 3 | |
3 | 1, 2 | sylan 488 | . 2 |
4 | df-f1 5893 | . . . 4 | |
5 | 4 | simprbi 480 | . . 3 |
6 | 5 | adantr 481 | . 2 |
7 | df-f1 5893 | . 2 | |
8 | 3, 6, 7 | sylanbrc 698 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wss 3574 ccnv 5113 wfun 5882 wf 5884 wf1 5885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-in 3581 df-ss 3588 df-f 5892 df-f1 5893 |
This theorem is referenced by: f1sng 6178 f1prex 6539 domssex2 8120 1sdom 8163 marypha1lem 8339 marypha2 8345 isinffi 8818 fseqenlem1 8847 dfac12r 8968 ackbij2 9065 cff1 9080 fin23lem28 9162 fin23lem41 9174 pwfseqlem5 9485 hashf1lem1 13239 gsumzres 18310 gsumzcl2 18311 gsumzf1o 18313 gsumzaddlem 18321 gsumzmhm 18337 gsumzoppg 18344 lindfres 20162 islindf3 20165 dvne0f1 23775 istrkg2ld 25359 ausgrusgrb 26060 uspgrushgr 26070 usgruspgr 26073 uspgr1e 26136 sizusglecusglem1 26357 qqhre 30064 erdsze2lem1 31185 eldioph2lem2 37324 eldioph2 37325 |
Copyright terms: Public domain | W3C validator |