Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | suppssr.f | |
|
suppssr.n | |
||
suppssr.a | |
||
suppssr.z | |
||
Assertion | suppssr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppssr.f | |
|
2 | suppssr.n | |
|
3 | suppssr.a | |
|
4 | suppssr.z | |
|
5 | eldif | |
|
6 | fvex | |
|
7 | eldifsn | |
|
8 | 6 7 | mpbiran | |
9 | 1 | ffnd | |
10 | elsuppfn | |
|
11 | 9 3 4 10 | syl3anc | |
12 | ibar | |
|
13 | 6 12 | mp1i | |
14 | 13 7 | bitr4di | |
15 | 14 | pm5.32da | |
16 | 11 15 | bitrd | |
17 | 2 | sseld | |
18 | 16 17 | sylbird | |
19 | 18 | expdimp | |
20 | 8 19 | syl5bir | |
21 | 20 | necon1bd | |
22 | 21 | impr | |
23 | 5 22 | sylan2b | |