Theorem nfs1v 1951

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

Syntax hints:   F/wnf 1471   [wsb 1773

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774

This theorem is referenced by:  nfsbxy  1954  nfsbxyt  1955  sbco3v  1981  sbcomxyyz  1984  sbnf2  1993  mo2n  2066  mo23  2079  mor  2080  clelab  2315  cbvralf  2710  cbvrexf  2711  cbvralsv  2734  cbvrexsv  2735  cbvrab  2750  sbhypf  2801  mob2  2932  reu2  2940  sbcralt  3054  sbcrext  3055  sbcralg  3056  sbcreug  3058  sbcel12g  3087  sbceqg  3088  cbvreucsf  3136  cbvrabcsf  3137  disjiun  4016  cbvopab1  4094  cbvopab1s  4096  csbopabg  4099  cbvmptf  4115  cbvmpt  4116  opelopabsb  4281  frind  4373  tfis  4603  findes  4623  opeliunxp  4702  ralxpf  4794  rexxpf  4795  cbviota  5204  csbiotag  5231  isarep1  5324  cbvriota  5866  csbriotag  5868  abrexex2g  6149  abrexex2  6153  dfoprab4f  6222  finexdc  6934  ssfirab  6966  uzind4s  9627  zsupcllemstep  11988  bezoutlemmain  12041  nnwosdc  12082  cbvrald  15044  bj-bdfindes  15205  bj-findes  15237