Description: Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elsuppfnd.1 | ||
elsuppfnd.2 | |||
elsuppfnd.3 | |||
elsuppfnd.4 | |||
elsuppfnd.5 | |||
Assertion | elsuppfnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsuppfnd.1 | ||
2 | elsuppfnd.2 | ||
3 | elsuppfnd.3 | ||
4 | elsuppfnd.4 | ||
5 | elsuppfnd.5 | ||
6 | elsuppfn | ||
7 | 6 | biimpar | |
8 | 1 2 3 4 5 7 | syl32anc |