Description: Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017) (Revised by AV, 1-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | suppss2f.p | |
|
suppss2f.a | |
||
suppss2f.w | |
||
suppss2f.n | |
||
suppss2f.v | |
||
Assertion | suppss2f | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppss2f.p | |
|
2 | suppss2f.a | |
|
3 | suppss2f.w | |
|
4 | suppss2f.n | |
|
5 | suppss2f.v | |
|
6 | nfcv | |
|
7 | nfcv | |
|
8 | nfcsb1v | |
|
9 | csbeq1a | |
|
10 | 2 6 7 8 9 | cbvmptf | |
11 | 10 | oveq1i | |
12 | 4 | sbt | |
13 | sbim | |
|
14 | sban | |
|
15 | 1 | sbf | |
16 | 2 3 | nfdif | |
17 | 16 | clelsb1fw | |
18 | 15 17 | anbi12i | |
19 | 14 18 | bitri | |
20 | sbsbc | |
|
21 | sbceq1g | |
|
22 | 21 | elv | |
23 | 20 22 | bitri | |
24 | 19 23 | imbi12i | |
25 | 13 24 | bitri | |
26 | 12 25 | mpbi | |
27 | 26 5 | suppss2 | |
28 | 11 27 | eqsstrid | |