Theorem nfs1v 1955

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

Step	Hyp	Ref	Expression
1		hbs1 1954	. 2 |- ( [ y / x ] ph -> A. x [ y / x ] ph )
2	1	nfi 1473	1 |- F/ x [ y / x ] ph

Syntax hints:   F/wnf 1471   [wsb 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774

This theorem is referenced by:  nfsbxy  1958  nfsbxyt  1959  sbco3v  1985  sbcomxyyz  1988  sbnf2  1997  mo2n  2070  mo23  2083  mor  2084  clelab  2319  cbvralf  2718  cbvrexf  2719  cbvralsv  2742  cbvrexsv  2743  cbvrab  2758  sbhypf  2810  mob2  2941  reu2  2949  sbcralt  3063  sbcrext  3064  sbcralg  3065  sbcreug  3067  sbcel12g  3096  sbceqg  3097  cbvreucsf  3146  cbvrabcsf  3147  disjiun  4025  cbvopab1  4103  cbvopab1s  4105  csbopabg  4108  cbvmptf  4124  cbvmpt  4125  opelopabsb  4291  frind  4384  tfis  4616  findes  4636  opeliunxp  4715  ralxpf  4809  rexxpf  4810  cbviota  5221  csbiotag  5248  isarep1  5341  cbvriota  5885  csbriotag  5887  abrexex2g  6174  abrexex2  6178  dfoprab4f  6248  finexdc  6960  ssfirab  6992  uzind4s  9658  zsupcllemstep  12085  bezoutlemmain  12138  nnwosdc  12179  cbvrald  15350  bj-bdfindes  15511  bj-findes  15543