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

Theorem nfsum 10332
 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-isum 10329 . 2 DECID
2 nfcv 2220 . . . . 5
3 nfsum.1 . . . . . . 7
4 nfcv 2220 . . . . . . 7
53, 4nfss 2993 . . . . . 6
63nfcri 2214 . . . . . . . 8
76nfdc 1590 . . . . . . 7 DECID
84, 7nfralxy 2403 . . . . . 6 DECID
9 nfcv 2220 . . . . . . . 8
10 nfcv 2220 . . . . . . . 8
113nfcri 2214 . . . . . . . . . 10
12 nfcv 2220 . . . . . . . . . . 11
13 nfsum.2 . . . . . . . . . . 11
1412, 13nfcsb 2941 . . . . . . . . . 10
15 nfcv 2220 . . . . . . . . . 10
1611, 14, 15nfif 3385 . . . . . . . . 9
172, 16nfmpt 3878 . . . . . . . 8
18 nfcv 2220 . . . . . . . 8
199, 10, 17, 18nfiseq 9528 . . . . . . 7
20 nfcv 2220 . . . . . . 7
21 nfcv 2220 . . . . . . 7
2219, 20, 21nfbr 3837 . . . . . 6
235, 8, 22nf3an 1499 . . . . 5 DECID
242, 23nfrexxy 2404 . . . 4 DECID
25 nfcv 2220 . . . . 5
26 nfcv 2220 . . . . . . . 8
27 nfcv 2220 . . . . . . . 8
2826, 27, 3nff1o 5155 . . . . . . 7
29 nfcv 2220 . . . . . . . . . 10
30 nfv 1462 . . . . . . . . . . . 12
31 nfcv 2220 . . . . . . . . . . . . 13
3231, 13nfcsb 2941 . . . . . . . . . . . 12
3330, 32, 15nfif 3385 . . . . . . . . . . 11
3425, 33nfmpt 3878 . . . . . . . . . 10
3529, 10, 34, 18nfiseq 9528 . . . . . . . . 9
3635, 9nffv 5216 . . . . . . . 8
3736nfeq2 2231 . . . . . . 7
3828, 37nfan 1498 . . . . . 6
3938nfex 1569 . . . . 5
4025, 39nfrexxy 2404 . . . 4
4124, 40nfor 1507 . . 3 DECID
4241nfiotaxy 4901 . 2 DECID
431, 42nfcxfr 2217 1
 Colors of variables: wff set class Syntax hints:   wa 102   wo 662  DECID wdc 776   w3a 920   wceq 1285  wex 1422   wcel 1434  wnfc 2207  wral 2349  wrex 2350  csb 2909   wss 2974  cif 3359   class class class wbr 3793   cmpt 3847  cio 4895  wf1o 4931  cfv 4932  (class class class)co 5543  cc 7041  cc0 7043  c1 7044   caddc 7046   cle 7216  cn 8106  cz 8432  cuz 8700  cfz 9105   cseq 9521   cli 10255  csu 10328 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-dc 777  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-rab 2358  df-v 2604  df-sbc 2817  df-csb 2910  df-un 2978  df-in 2980  df-ss 2987  df-if 3360  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-opab 3848  df-mpt 3849  df-xp 4377  df-rel 4378  df-cnv 4379  df-co 4380  df-dm 4381  df-rn 4382  df-res 4383  df-iota 4897  df-fun 4934  df-fn 4935  df-f 4936  df-f1 4937  df-fo 4938  df-f1o 4939  df-fv 4940  df-ov 5546  df-oprab 5547  df-mpt2 5548  df-recs 5954  df-frec 6040  df-iseq 9522  df-isum 10329 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator