Theorem nfs1v 1958

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

Syntax hints:   F/wnf 1474   [wsb 1776

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777

This theorem is referenced by:  nfsbxy  1961  nfsbxyt  1962  sbco3v  1988  sbcomxyyz  1991  sbnf2  2000  mo2n  2073  mo23  2086  mor  2087  clelab  2322  cbvralf  2721  cbvrexf  2722  cbvralsv  2745  cbvrexsv  2746  cbvrab  2761  sbhypf  2813  mob2  2944  reu2  2952  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcreug  3070  sbcel12g  3099  sbceqg  3100  cbvreucsf  3149  cbvrabcsf  3150  disjiun  4028  cbvopab1  4106  cbvopab1s  4108  csbopabg  4111  cbvmptf  4127  cbvmpt  4128  opelopabsb  4294  frind  4387  tfis  4619  findes  4639  opeliunxp  4718  ralxpf  4812  rexxpf  4813  cbviota  5224  csbiotag  5251  isarep1  5344  cbvriota  5888  csbriotag  5890  abrexex2g  6177  abrexex2  6181  dfoprab4f  6251  finexdc  6963  ssfirab  6997  uzind4s  9664  zsupcllemstep  10319  bezoutlemmain  12165  nnwosdc  12206  cbvrald  15434  bj-bdfindes  15595  bj-findes  15627