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

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

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 1856 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1392 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1390   [wsb 1686
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-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687
This theorem is referenced by:  nfsbxy  1860  nfsbxyt  1861  sbco3v  1885  sbcomxyyz  1888  sbnf2  1899  mo2n  1970  mo23  1983  mor  1984  clelab  2204  cbvralf  2572  cbvrexf  2573  cbvralsv  2589  cbvrexsv  2590  cbvrab  2600  sbhypf  2649  mob2  2773  reu2  2781  sbcralt  2891  sbcrext  2892  sbcralg  2893  sbcreug  2895  sbcel12g  2922  sbceqg  2923  cbvreucsf  2967  cbvrabcsf  2968  cbvopab1  3859  cbvopab1s  3861  csbopabg  3864  cbvmpt  3880  opelopabsb  4023  frind  4115  tfis  4332  findes  4352  opeliunxp  4421  ralxpf  4510  rexxpf  4511  cbviota  4902  csbiotag  4925  isarep1  5016  cbvriota  5509  csbriotag  5511  abrexex2g  5778  abrexex2  5782  dfoprab4f  5850  uzind4s  8759  zsupcllemstep  10485  bezoutlemmain  10531  cbvrald  10776  bj-bdfindes  10929  bj-findes  10961
  Copyright terms: Public domain W3C validator