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  4348  frind  4443  tfis  4675  findes  4695  opeliunxp  4774  ralxpf  4868  rexxpf  4869  cbviota  5283  csbiotag  5311  isarep1  5407  cbvriota  5972  csbriotag  5974  abrexex2g  6271  abrexex2  6275  dfoprab4f  6345  finexdc  7072  ssfirab  7106  uzind4s  9793  zsupcllemstep  10457  bezoutlemmain  12529  nnwosdc  12570  cbvrald  16178  bj-bdfindes  16338  bj-findes  16370