Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfsum Unicode version

Theorem nfsum 9876
 Description: Bound-variable hypothesis builder for sum: if is (effectively) not free in and , it is not free in . (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Hypotheses
Ref Expression
nfsum.1
nfsum.2
Assertion
Ref Expression
nfsum

Proof of Theorem nfsum
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 9873 . 2
2 nfcv 2178 . . . . 5
3 nfsum.1 . . . . . . 7
4 nfcv 2178 . . . . . . 7
53, 4nfss 2938 . . . . . 6
6 nfcv 2178 . . . . . . . 8
7 nfcv 2178 . . . . . . . 8
83nfcri 2172 . . . . . . . . . 10
9 nfcv 2178 . . . . . . . . . . 11
10 nfsum.2 . . . . . . . . . . 11
119, 10nfcsb 2884 . . . . . . . . . 10
12 nfcv 2178 . . . . . . . . . 10
138, 11, 12nfif 3356 . . . . . . . . 9
142, 13nfmpt 3849 . . . . . . . 8
15 nfcv 2178 . . . . . . . 8
166, 7, 14, 15nfiseq 9218 . . . . . . 7
17 nfcv 2178 . . . . . . 7
18 nfcv 2178 . . . . . . 7
1916, 17, 18nfbr 3808 . . . . . 6
205, 19nfan 1457 . . . . 5
212, 20nfrexya 2363 . . . 4
22 nfcv 2178 . . . . 5
23 nfcv 2178 . . . . . . . 8
24 nfcv 2178 . . . . . . . 8
2523, 24, 3nff1o 5124 . . . . . . 7
26 nfcv 2178 . . . . . . . . . 10
27 nfcv 2178 . . . . . . . . . . . 12
2827, 10nfcsb 2884 . . . . . . . . . . 11
2922, 28nfmpt 3849 . . . . . . . . . 10
3026, 7, 29, 15nfiseq 9218 . . . . . . . . 9
3130, 6nffv 5185 . . . . . . . 8
3231nfeq2 2189 . . . . . . 7
3325, 32nfan 1457 . . . . . 6
3433nfex 1528 . . . . 5
3522, 34nfrexya 2363 . . . 4
3621, 35nfor 1466 . . 3
3736nfiotaxy 4871 . 2
381, 37nfcxfr 2175 1
 Colors of variables: wff set class Syntax hints:   wa 97   wo 629   wceq 1243  wex 1381   wcel 1393  wnfc 2165  wrex 2307  csb 2852   wss 2917  cif 3331   class class class wbr 3764   cmpt 3818  cio 4865  wf1o 4901  cfv 4902  (class class class)co 5512  cc 6887  cc0 6889  c1 6890   caddc 6892  cn 7914  cz 8245  cuz 8473  cfz 8874   cseq 9211   cli 9799  csu 9872 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-un 2922  df-in 2924  df-ss 2931  df-if 3332  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-opab 3819  df-mpt 3820  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-recs 5920  df-frec 5978  df-iseq 9212  df-sum 9873 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator