Theorem nfs1v 1793

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

Syntax hints:   F/wnf 1325  [wsb 1623

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 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405

This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624

This theorem is referenced by:  nfsbxy  1796  nfsbxyt  1797  sbco3v  1821  sbcomxyyz  1824  sbnf2  1835  mo2n  1906  mo23  1919  mor  1920  clelab  2140  cbvralf  2501  cbvrexf  2502  cbvralsv  2518  cbvrexsv  2519  cbvrab  2529  sbhypf  2576  mob2  2694  reu2  2702  sbcralt  2807  sbcrext  2808  sbcralg  2809  sbcrexg  2810  sbcreug  2811  sbcel12g  2838  sbceqg  2839  cbvreucsf  2883  cbvrabcsf  2884  cbvopab1  3800  cbvopab1s  3802  csbopabg  3805  cbvmpt  3821  opelopabsb  3967  tfis  4229  findes  4249  opeliunxp  4318  ralxpf  4405  rexxpf  4406  cbviota  4795  csbiotag  4818  isarep1  4907  cbvriota  5398  csbriotag  5400  abrexex2g  5666  abrexex2  5670  dfoprab4f  5738  cbvrald  7226  bj-bdfindes  7367  bj-findes  7395