Theorem nfs1v 1913

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

Syntax hints:   F/wnf 1437   [wsb 1736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737

This theorem is referenced by:  nfsbxy  1916  nfsbxyt  1917  sbco3v  1943  sbcomxyyz  1946  sbnf2  1957  mo2n  2028  mo23  2041  mor  2042  clelab  2266  cbvralf  2651  cbvrexf  2652  cbvralsv  2671  cbvrexsv  2672  cbvrab  2687  sbhypf  2738  mob2  2868  reu2  2876  sbcralt  2989  sbcrext  2990  sbcralg  2991  sbcreug  2993  sbcel12g  3022  sbceqg  3023  cbvreucsf  3069  cbvrabcsf  3070  disjiun  3932  cbvopab1  4009  cbvopab1s  4011  csbopabg  4014  cbvmptf  4030  cbvmpt  4031  opelopabsb  4190  frind  4282  tfis  4505  findes  4525  opeliunxp  4602  ralxpf  4693  rexxpf  4694  cbviota  5101  csbiotag  5124  isarep1  5217  cbvriota  5748  csbriotag  5750  abrexex2g  6026  abrexex2  6030  dfoprab4f  6099  finexdc  6804  ssfirab  6830  uzind4s  9412  zsupcllemstep  11674  bezoutlemmain  11722  cbvrald  13166  bj-bdfindes  13318  bj-findes  13350