Theorem nfs1v 1958

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

Syntax hints:   F/wnf 1474   [wsb 1776

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777

This theorem is referenced by:  nfsbxy  1961  nfsbxyt  1962  sbco3v  1988  sbcomxyyz  1991  sbnf2  2000  mo2n  2073  mo23  2086  mor  2087  clelab  2322  cbvralf  2721  cbvrexf  2722  cbvralsv  2745  cbvrexsv  2746  cbvrab  2761  sbhypf  2813  mob2  2944  reu2  2952  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcreug  3070  sbcel12g  3099  sbceqg  3100  cbvreucsf  3149  cbvrabcsf  3150  disjiun  4029  cbvopab1  4107  cbvopab1s  4109  csbopabg  4112  cbvmptf  4128  cbvmpt  4129  opelopabsb  4295  frind  4388  tfis  4620  findes  4640  opeliunxp  4719  ralxpf  4813  rexxpf  4814  cbviota  5225  csbiotag  5252  isarep1  5345  cbvriota  5891  csbriotag  5893  abrexex2g  6186  abrexex2  6190  dfoprab4f  6260  finexdc  6972  ssfirab  7006  uzind4s  9681  zsupcllemstep  10336  bezoutlemmain  12190  nnwosdc  12231  cbvrald  15518  bj-bdfindes  15679  bj-findes  15711