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

Theorem nfs1v 1797
Description: x is not free in [y / x]φ when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfs1v x[y / x]φ
Distinct variable group:   x,y
Allowed substitution hints:   φ(x,y)

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 1796 . 2 ([y / x]φx[y / x]φ)
21nfi 1331 1 x[y / x]φ
Colors of variables: wff set class
Syntax hints:  wnf 1329  [wsb 1627
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-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628
This theorem is referenced by:  nfsbxy  1800  nfsbxyt  1801  sbco3v  1825  sbcomxyyz  1828  sbnf2  1839  mo2n  1910  mo23  1923  mor  1924  clelab  2144  cbvralf  2505  cbvrexf  2506  cbvralsv  2522  cbvrexsv  2523  cbvrab  2533  sbhypf  2580  mob2  2698  reu2  2706  sbcralt  2811  sbcrext  2812  sbcralg  2813  sbcrexg  2814  sbcreug  2815  sbcel12g  2842  sbceqg  2843  cbvreucsf  2887  cbvrabcsf  2888  cbvopab1  3804  cbvopab1s  3806  csbopabg  3809  cbvmpt  3825  opelopabsb  3971  tfis  4233  findes  4253  opeliunxp  4322  ralxpf  4409  rexxpf  4410  cbviota  4799  csbiotag  4822  isarep1  4911  cbvriota  5402  csbriotag  5404  abrexex2g  5670  abrexex2  5674  dfoprab4f  5742  cbvrald  7034  bj-bdfindes  7171  bj-findes  7199
  Copyright terms: Public domain W3C validator