Theorem nfs1v 1993

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

Syntax hints:   F/wnf 1509   [wsb 1811

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  nfsbxy  1996  nfsbxyt  1997  sbco3v  2023  sbcomxyyz  2026  sbnf2  2035  mo2n  2108  mo23  2122  mor  2123  clelab  2360  cbvralf  2769  cbvrexf  2770  cbvralsv  2794  cbvrexsv  2795  cbvrab  2811  sbhypf  2864  mob2  2997  reu2  3005  sbcralt  3119  sbcrext  3120  sbcralg  3121  sbcreug  3123  sbcel12g  3153  sbceqg  3154  cbvreucsf  3203  cbvrabcsf  3204  disjiun  4104  cbvopab1  4183  cbvopab1s  4185  csbopabg  4188  cbvmptf  4204  cbvmpt  4205  opelopabsb  4378  frind  4473  tfis  4705  findes  4725  opeliunxp  4805  ralxpf  4901  rexxpf  4902  cbviota  5317  csbiotag  5345  isarep1  5442  cbvriota  6015  csbriotag  6017  abrexex2g  6313  abrexex2  6317  dfoprab4f  6387  modom  7061  finexdc  7160  ssfirab  7197  uzind4s  9922  zsupcllemstep  10589  bezoutlemmain  12694  nnwosdc  12735  cbvrald  16560  bj-bdfindes  16719  bj-findes  16751