Theorem nfs1v 2146

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

Syntax hints:   F/wnf 1594   [wsb 1701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-12 1793  ax-13 1944

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1702

This theorem is referenced by:  sbnf2OLD  2149  mo3  2294  mo3OLD  2295  eu1  2300  eu1OLD  2301  moOLD  2302  mopickOLD  2339  2mo  2357  2moOLD  2358  2eu6  2365  clelab  2555  cbvralf  2933  cbvralsv  2950  cbvrexsv  2951  cbvrab  2962  sbhypf  3010  mob2  3130  reu2  3138  sbcralt  3257  sbcrexgOLD  3262  sbcreu  3263  sbcreugOLD  3264  cbvreucsf  3311  cbvrabcsf  3312  sbcel12  3665  sbcel12gOLD  3666  sbceqg  3667  csbif  3829  csbifgOLD  3830  cbvopab1  4352  cbvopab1s  4354  cbvmpt  4372  opelopabsb  4590  csbopab  4611  csbopabgOLD  4612  opeliunxp  4879  ralxpf  4975  cbviota  5376  csbiota  5400  csbiotagOLD  5401  isarep1  5487  cbvriota  6052  csbriota  6054  onminex  6409  tfis  6456  findes  6497  abrexex2g  6545  abrexex2  6549  dfoprab4f  6623  axrepndlem1  8746  axrepndlem2  8747  uzind4s  10904  mo5f  25694  cbvmptf  25797  esumcvg  26391  wl-mo3t  28243  sbcalf  28766  sbcexf  28767  rabasiun  30078  opeliun2xp  30567  2sb5nd  31010  2sb5ndALT  31410