Description: Taking the converse image of a set can be limited to the range of the function used. (Contributed by Thierry Arnoux, 17-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | fimacnvinrn2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inass | |
|
2 | sseqin2 | |
|
3 | 2 | biimpi | |
4 | 3 | adantl | |
5 | 4 | ineq2d | |
6 | 1 5 | eqtrid | |
7 | 6 | imaeq2d | |
8 | fimacnvinrn | |
|
9 | 8 | adantr | |
10 | fimacnvinrn | |
|
11 | 10 | adantr | |
12 | 7 9 11 | 3eqtr4rd | |