Theorem nfs1v 1968

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

Syntax hints:   F/wnf 1484   [wsb 1786

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787

This theorem is referenced by:  nfsbxy  1971  nfsbxyt  1972  sbco3v  1998  sbcomxyyz  2001  sbnf2  2010  mo2n  2083  mo23  2096  mor  2097  clelab  2332  cbvralf  2731  cbvrexf  2732  cbvralsv  2755  cbvrexsv  2756  cbvrab  2771  sbhypf  2824  mob2  2955  reu2  2963  sbcralt  3077  sbcrext  3078  sbcralg  3079  sbcreug  3081  sbcel12g  3110  sbceqg  3111  cbvreucsf  3160  cbvrabcsf  3161  disjiun  4043  cbvopab1  4122  cbvopab1s  4124  csbopabg  4127  cbvmptf  4143  cbvmpt  4144  opelopabsb  4311  frind  4404  tfis  4636  findes  4656  opeliunxp  4735  ralxpf  4829  rexxpf  4830  cbviota  5243  csbiotag  5270  isarep1  5366  cbvriota  5920  csbriotag  5922  abrexex2g  6215  abrexex2  6219  dfoprab4f  6289  finexdc  7011  ssfirab  7045  uzind4s  9724  zsupcllemstep  10385  bezoutlemmain  12369  nnwosdc  12410  cbvrald  15838  bj-bdfindes  15999  bj-findes  16031