Theorem nfs1v 1812

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

Syntax hints:   F/wnf 1346  [wsb 1642

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643

This theorem is referenced by:  nfsbxy  1815  nfsbxyt  1816  sbco3v  1840  sbcomxyyz  1843  sbnf2  1854  mo2n  1925  mo23  1938  mor  1939  clelab  2159  cbvralf  2521  cbvrexf  2522  cbvralsv  2538  cbvrexsv  2539  cbvrab  2549  sbhypf  2597  mob2  2715  reu2  2723  sbcralt  2828  sbcrext  2829  sbcralg  2830  sbcrexg  2831  sbcreug  2832  sbcel12g  2859  sbceqg  2860  cbvreucsf  2904  cbvrabcsf  2905  cbvopab1  3821  cbvopab1s  3823  csbopabg  3826  cbvmpt  3842  opelopabsb  3988  tfis  4249  findes  4269  opeliunxp  4338  ralxpf  4425  rexxpf  4426  cbviota  4815  csbiotag  4838  isarep1  4928  cbvriota  5421  csbriotag  5423  abrexex2g  5689  abrexex2  5693  dfoprab4f  5761  uzind4s  8309  cbvrald  9262  bj-bdfindes  9409  bj-findes  9441