![]() |
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 5801 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fss 5759 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan 478 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-f1 5605 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | simprbi 470 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | adantr 471 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | df-f1 5605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 3, 6, 7 | sylanbrc 675 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-in 3422 df-ss 3429 df-f 5604 df-f1 5605 |
This theorem is referenced by: f1prex 6206 domssex2 7757 1sdom 7800 marypha1lem 7972 marypha2 7978 isinffi 8451 fseqenlem1 8480 dfac12r 8601 ackbij2 8698 cff1 8713 fin23lem28 8795 fin23lem41 8807 pwfseqlem5 9113 hashf1lem1 12650 gsumzres 17591 gsumzcl2 17592 gsumzf1o 17594 gsumzaddlem 17602 gsumzmhm 17618 gsumzoppg 17625 lindfres 19429 islindf3 19432 dvne0f1 23012 istrkg2ld 24556 ausisusgra 25130 uslisushgra 25138 usisuslgra 25140 uslgra1 25147 usgra1 25148 sizeusglecusglem1 25260 2trllemE 25331 constr1trl 25366 frgrancvvdeqlem8 25816 qqhre 28872 erdsze2lem1 29974 eldioph2lem2 35647 eldioph2 35648 ausgrusgrb 39299 uspgrushgr 39309 usgruspgr 39312 uspgr1e 39368 sizusglecusglem1 39571 |
Copyright terms: Public domain | W3C validator |