Theorem nfs1v 1995

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

Syntax hints:   F/wnf 1509   [wsb 1811

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  nfsbxy  1998  nfsbxyt  1999  sbco3v  2025  sbcomxyyz  2028  sbnf2  2037  mo2n  2110  mo23  2124  mor  2125  clelab  2362  cbvralf  2771  cbvrexf  2772  cbvralsv  2796  cbvrexsv  2797  cbvrab  2813  sbhypf  2866  mob2  3000  reu2  3008  sbcralt  3122  sbcrext  3123  sbcralg  3124  sbcreug  3126  sbcel12g  3156  sbceqg  3157  cbvreucsf  3206  cbvrabcsf  3207  disjiun  4110  cbvopab1  4189  cbvopab1s  4191  csbopabg  4194  cbvmptf  4210  cbvmpt  4211  opelopabsb  4384  frind  4479  tfis  4712  findes  4732  opeliunxp  4812  ralxpf  4908  rexxpf  4909  cbviota  5324  csbiotag  5352  isarep1  5449  cbvriota  6025  csbriotag  6027  abrexex2g  6324  abrexex2  6328  dfoprab4f  6402  modom  7076  finexdc  7175  ssfirab  7212  uzind4s  9945  zsupcllemstep  10616  bezoutlemmain  12725  nnwosdc  12766  cbvrald  16702  bj-bdfindes  16861  bj-findes  16893