Theorem nfs1v 1990

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

Syntax hints:   F/wnf 1506   [wsb 1808

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809

This theorem is referenced by:  nfsbxy  1993  nfsbxyt  1994  sbco3v  2020  sbcomxyyz  2023  sbnf2  2032  mo2n  2105  mo23  2119  mor  2120  clelab  2355  cbvralf  2756  cbvrexf  2757  cbvralsv  2781  cbvrexsv  2782  cbvrab  2797  sbhypf  2850  mob2  2983  reu2  2991  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcreug  3109  sbcel12g  3139  sbceqg  3140  cbvreucsf  3189  cbvrabcsf  3190  disjiun  4077  cbvopab1  4156  cbvopab1s  4158  csbopabg  4161  cbvmptf  4177  cbvmpt  4178  opelopabsb  4347  frind  4440  tfis  4672  findes  4692  opeliunxp  4771  ralxpf  4865  rexxpf  4866  cbviota  5279  csbiotag  5307  isarep1  5403  cbvriota  5959  csbriotag  5961  abrexex2g  6255  abrexex2  6259  dfoprab4f  6329  finexdc  7052  ssfirab  7086  uzind4s  9773  zsupcllemstep  10436  bezoutlemmain  12505  nnwosdc  12546  cbvrald  16082  bj-bdfindes  16242  bj-findes  16274