Description: Bound-variable hypothesis builder for sum: if x is (effectively) not free in A and B , it is not free in sum_ k e. A B . Version of nfsum with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 11-Dec-2005) (Revised by Gino Giotto, 24-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfsum.1 | |
|
nfsum.2 | |
||
Assertion | nfsum | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsum.1 | |
|
2 | nfsum.2 | |
|
3 | df-sum | |
|
4 | nfcv | |
|
5 | nfcv | |
|
6 | 1 5 | nfss | |
7 | nfcv | |
|
8 | nfcv | |
|
9 | 1 | nfcri | |
10 | nfcv | |
|
11 | 10 2 | nfcsbw | |
12 | nfcv | |
|
13 | 9 11 12 | nfif | |
14 | 4 13 | nfmpt | |
15 | 7 8 14 | nfseq | |
16 | nfcv | |
|
17 | nfcv | |
|
18 | 15 16 17 | nfbr | |
19 | 6 18 | nfan | |
20 | 4 19 | nfrex | |
21 | nfcv | |
|
22 | nfcv | |
|
23 | nfcv | |
|
24 | 22 23 1 | nff1o | |
25 | nfcv | |
|
26 | nfcv | |
|
27 | 26 2 | nfcsbw | |
28 | 21 27 | nfmpt | |
29 | 25 8 28 | nfseq | |
30 | 29 7 | nffv | |
31 | 30 | nfeq2 | |
32 | 24 31 | nfan | |
33 | 32 | nfex | |
34 | 21 33 | nfrex | |
35 | 20 34 | nfor | |
36 | 35 | nfiotaw | |
37 | 3 36 | nfcxfr | |