Theorem nfs1v 2266

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

Syntax hints:   F/wnf 1667   [wsb 1797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933  ax-13 2091

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-sb 1798

This theorem is referenced by:  mo3  2336  eu1  2339  2mo  2380  2eu6  2387  cbvralf  3013  cbvralsv  3030  cbvrexsv  3031  cbvrab  3043  sbhypf  3095  mob2  3218  reu2  3226  reu2eqd  3235  sbcralt  3340  sbcreu  3344  cbvreucsf  3397  cbvrabcsf  3398  sbcel12  3772  sbceqg  3773  csbif  3931  rabasiun  4282  cbvopab1  4473  cbvopab1s  4475  cbvmptf  4493  cbvmpt  4494  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  opeliunxp  4886  ralxpf  4981  cbviota  5551  csbiota  5575  isarep1  5662  cbvriota  6262  csbriota  6264  onminex  6634  tfis  6681  findes  6723  abrexex2g  6770  abrexex2  6774  dfoprab4f  6851  axrepndlem1  9017  axrepndlem2  9018  uzind4s  11219  mo5f  28120  ac6sf2  28226  esumcvg  28907  bj-mo3OLD  31447  wl-lem-moexsb  31897  wl-mo3t  31905  poimirlem26  31966  sbcalf  32352  sbcexf  32353  sbcrexgOLD  35628  sbcel12gOLD  36905  2sb5nd  36927  2sb5ndALT  37329  opeliun2xp  40167