Theorem nfs1v 1927

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 1926	. 2 |- ( [ y / x ] ph -> A. x [ y / x ] ph )
2	1	nfi 1450	1 |- F/ x [ y / x ] ph

Syntax hints:   F/wnf 1448   [wsb 1750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751

This theorem is referenced by:  nfsbxy  1930  nfsbxyt  1931  sbco3v  1957  sbcomxyyz  1960  sbnf2  1969  mo2n  2042  mo23  2055  mor  2056  clelab  2292  cbvralf  2685  cbvrexf  2686  cbvralsv  2708  cbvrexsv  2709  cbvrab  2724  sbhypf  2775  mob2  2906  reu2  2914  sbcralt  3027  sbcrext  3028  sbcralg  3029  sbcreug  3031  sbcel12g  3060  sbceqg  3061  cbvreucsf  3109  cbvrabcsf  3110  disjiun  3977  cbvopab1  4055  cbvopab1s  4057  csbopabg  4060  cbvmptf  4076  cbvmpt  4077  opelopabsb  4238  frind  4330  tfis  4560  findes  4580  opeliunxp  4659  ralxpf  4750  rexxpf  4751  cbviota  5158  csbiotag  5181  isarep1  5274  cbvriota  5808  csbriotag  5810  abrexex2g  6088  abrexex2  6092  dfoprab4f  6161  finexdc  6868  ssfirab  6899  uzind4s  9528  zsupcllemstep  11878  bezoutlemmain  11931  nnwosdc  11972  cbvrald  13669  bj-bdfindes  13831  bj-findes  13863