ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfsb Structured version   GIF version

Theorem nfsb 1800
Description: If z is not free in φ, it is not free in [y / x]φ when y and z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
Hypothesis
Ref Expression
nfsb.1 zφ
Assertion
Ref Expression
nfsb z[y / x]φ
Distinct variable group:   y,z
Allowed substitution hints:   φ(x,y,z)

Proof of Theorem nfsb
Dummy variable w is distinct from all other variables.
StepHypRef Expression
1 nfsb.1 . . . 4 zφ
21nfsbxy 1796 . . 3 z[w / x]φ
32nfsbxy 1796 . 2 z[y / w][w / x]φ
4 ax-17 1396 . . . 4 (φwφ)
54sbco2v 1799 . . 3 ([y / w][w / x]φ ↔ [y / x]φ)
65nfbii 1338 . 2 (Ⅎz[y / w][w / x]φ ↔ Ⅎz[y / x]φ)
73, 6mpbi 133 1 z[y / x]φ
Colors of variables: wff set class
Syntax hints:  wnf 1325  [wsb 1623
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-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624
This theorem is referenced by:  hbsb  1801  sbco2yz  1815  sbcomxyyz  1824  hbsbd  1836  nfsb4or  1877  sb8eu  1891  nfeu  1897  cbvab  2138  cbvralf  2501  cbvrexf  2502  cbvreu  2505  cbvralsv  2518  cbvrexsv  2519  cbvrab  2529  cbvreucsf  2883  cbvrabcsf  2884  cbvopab1  3800  cbvmpt  3821  ralxpf  4405  rexxpf  4406  cbviota  4795  sb8iota  4797  cbvriota  5398  dfoprab4f  5738
  Copyright terms: Public domain W3C validator