Theorem nfs1v 1939

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

Syntax hints:   F/wnf 1460   [wsb 1762

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763

This theorem is referenced by:  nfsbxy  1942  nfsbxyt  1943  sbco3v  1969  sbcomxyyz  1972  sbnf2  1981  mo2n  2054  mo23  2067  mor  2068  clelab  2303  cbvralf  2696  cbvrexf  2697  cbvralsv  2719  cbvrexsv  2720  cbvrab  2735  sbhypf  2786  mob2  2917  reu2  2925  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcreug  3043  sbcel12g  3072  sbceqg  3073  cbvreucsf  3121  cbvrabcsf  3122  disjiun  3998  cbvopab1  4076  cbvopab1s  4078  csbopabg  4081  cbvmptf  4097  cbvmpt  4098  opelopabsb  4260  frind  4352  tfis  4582  findes  4602  opeliunxp  4681  ralxpf  4773  rexxpf  4774  cbviota  5183  csbiotag  5209  isarep1  5302  cbvriota  5840  csbriotag  5842  abrexex2g  6120  abrexex2  6124  dfoprab4f  6193  finexdc  6901  ssfirab  6932  uzind4s  9588  zsupcllemstep  11940  bezoutlemmain  11993  nnwosdc  12034  cbvrald  14422  bj-bdfindes  14583  bj-findes  14615