Theorem nfs1v 1992

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

Syntax hints:   F/wnf 1508   [wsb 1810

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811

This theorem is referenced by:  nfsbxy  1995  nfsbxyt  1996  sbco3v  2022  sbcomxyyz  2025  sbnf2  2034  mo2n  2107  mo23  2121  mor  2122  clelab  2357  cbvralf  2758  cbvrexf  2759  cbvralsv  2783  cbvrexsv  2784  cbvrab  2800  sbhypf  2853  mob2  2986  reu2  2994  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcreug  3112  sbcel12g  3142  sbceqg  3143  cbvreucsf  3192  cbvrabcsf  3193  disjiun  4083  cbvopab1  4162  cbvopab1s  4164  csbopabg  4167  cbvmptf  4183  cbvmpt  4184  opelopabsb  4354  frind  4449  tfis  4681  findes  4701  opeliunxp  4781  ralxpf  4876  rexxpf  4877  cbviota  5291  csbiotag  5319  isarep1  5416  cbvriota  5982  csbriotag  5984  abrexex2g  6281  abrexex2  6285  dfoprab4f  6355  modom  6993  finexdc  7091  ssfirab  7128  uzind4s  9823  zsupcllemstep  10488  bezoutlemmain  12568  nnwosdc  12609  cbvrald  16384  bj-bdfindes  16544  bj-findes  16576