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  4078  cbvopab1  4157  cbvopab1s  4159  csbopabg  4162  cbvmptf  4178  cbvmpt  4179  opelopabsb  4349  frind  4444  tfis  4676  findes  4696  opeliunxp  4776  ralxpf  4871  rexxpf  4872  cbviota  5286  csbiotag  5314  isarep1  5410  cbvriota  5975  csbriotag  5977  abrexex2g  6274  abrexex2  6278  dfoprab4f  6348  finexdc  7078  ssfirab  7114  uzind4s  9802  zsupcllemstep  10466  bezoutlemmain  12540  nnwosdc  12581  cbvrald  16261  bj-bdfindes  16421  bj-findes  16453