Metamath Proof Explorer


Theorem nfsum

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 _xA
nfsum.2 _xB
Assertion nfsum _xkAB

Proof

Step Hyp Ref Expression
1 nfsum.1 _xA
2 nfsum.2 _xB
3 df-sum kAB=ιz|mAmseqm+nifnAn/kB0zmff:1m1-1 ontoAz=seq1+nfn/kBm
4 nfcv _x
5 nfcv _xm
6 1 5 nfss xAm
7 nfcv _xm
8 nfcv _x+
9 1 nfcri xnA
10 nfcv _xn
11 10 2 nfcsbw _xn/kB
12 nfcv _x0
13 9 11 12 nfif _xifnAn/kB0
14 4 13 nfmpt _xnifnAn/kB0
15 7 8 14 nfseq _xseqm+nifnAn/kB0
16 nfcv _x
17 nfcv _xz
18 15 16 17 nfbr xseqm+nifnAn/kB0z
19 6 18 nfan xAmseqm+nifnAn/kB0z
20 4 19 nfrex xmAmseqm+nifnAn/kB0z
21 nfcv _x
22 nfcv _xf
23 nfcv _x1m
24 22 23 1 nff1o xf:1m1-1 ontoA
25 nfcv _x1
26 nfcv _xfn
27 26 2 nfcsbw _xfn/kB
28 21 27 nfmpt _xnfn/kB
29 25 8 28 nfseq _xseq1+nfn/kB
30 29 7 nffv _xseq1+nfn/kBm
31 30 nfeq2 xz=seq1+nfn/kBm
32 24 31 nfan xf:1m1-1 ontoAz=seq1+nfn/kBm
33 32 nfex xff:1m1-1 ontoAz=seq1+nfn/kBm
34 21 33 nfrex xmff:1m1-1 ontoAz=seq1+nfn/kBm
35 20 34 nfor xmAmseqm+nifnAn/kB0zmff:1m1-1 ontoAz=seq1+nfn/kBm
36 35 nfiotaw _xιz|mAmseqm+nifnAn/kB0zmff:1m1-1 ontoAz=seq1+nfn/kBm
37 3 36 nfcxfr _xkAB