Theorem nfs1v 1815

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

Syntax hints:   F/wnf 1349   [wsb 1645

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646

This theorem is referenced by:  nfsbxy  1818  nfsbxyt  1819  sbco3v  1843  sbcomxyyz  1846  sbnf2  1857  mo2n  1928  mo23  1941  mor  1942  clelab  2162  cbvralf  2527  cbvrexf  2528  cbvralsv  2544  cbvrexsv  2545  cbvrab  2555  sbhypf  2603  mob2  2721  reu2  2729  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcreug  2838  sbcel12g  2865  sbceqg  2866  cbvreucsf  2910  cbvrabcsf  2911  cbvopab1  3830  cbvopab1s  3832  csbopabg  3835  cbvmpt  3851  opelopabsb  3997  frind  4089  tfis  4306  findes  4326  opeliunxp  4395  ralxpf  4482  rexxpf  4483  cbviota  4872  csbiotag  4895  isarep1  4985  cbvriota  5478  csbriotag  5480  abrexex2g  5747  abrexex2  5751  dfoprab4f  5819  uzind4s  8533  cbvrald  9927  bj-bdfindes  10074  bj-findes  10106