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

Theorem nfs1v 1863
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 1862 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1396 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1394   [wsb 1692
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693
This theorem is referenced by:  nfsbxy  1866  nfsbxyt  1867  sbco3v  1891  sbcomxyyz  1894  sbnf2  1905  mo2n  1976  mo23  1989  mor  1990  clelab  2212  cbvralf  2584  cbvrexf  2585  cbvralsv  2601  cbvrexsv  2602  cbvrab  2617  sbhypf  2668  mob2  2795  reu2  2803  sbcralt  2915  sbcrext  2916  sbcralg  2917  sbcreug  2919  sbcel12g  2946  sbceqg  2947  cbvreucsf  2992  cbvrabcsf  2993  disjiun  3840  cbvopab1  3911  cbvopab1s  3913  csbopabg  3916  cbvmptf  3932  cbvmpt  3933  opelopabsb  4087  frind  4179  tfis  4398  findes  4418  opeliunxp  4493  ralxpf  4582  rexxpf  4583  cbviota  4985  csbiotag  5008  isarep1  5100  cbvriota  5618  csbriotag  5620  abrexex2g  5891  abrexex2  5895  dfoprab4f  5963  finexdc  6616  ssfirab  6641  uzind4s  9076  zsupcllemstep  11215  bezoutlemmain  11261  cbvrald  11643  bj-bdfindes  11799  bj-findes  11831
  Copyright terms: Public domain W3C validator