Theorem nfs1v 2286

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

Syntax hints:   F/wnf 1675   [wsb 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-13 2104

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806

This theorem is referenced by:  mo3  2356  eu1  2359  2mo  2400  2eu6  2407  cbvralf  2999  cbvralsv  3016  cbvrexsv  3017  cbvrab  3029  sbhypf  3081  mob2  3206  reu2  3214  reu2eqd  3223  sbcralt  3328  sbcreu  3332  cbvreucsf  3383  cbvrabcsf  3384  sbcel12  3776  sbceqg  3777  csbif  3922  rabasiun  4273  cbvopab1  4466  cbvopab1s  4468  cbvmptf  4486  cbvmpt  4487  opelopabsb  4711  csbopab  4733  csbopabgALT  4734  opeliunxp  4891  ralxpf  4986  cbviota  5558  csbiota  5582  isarep1  5672  cbvriota  6280  csbriota  6282  onminex  6653  tfis  6700  findes  6742  abrexex2g  6789  abrexex2  6793  dfoprab4f  6870  axrepndlem1  9035  axrepndlem2  9036  uzind4s  11242  mo5f  28199  ac6sf2  28302  esumcvg  28981  bj-mo3OLD  31515  wl-lem-moexsb  31967  wl-mo3t  31975  poimirlem26  32030  sbcalf  32416  sbcexf  32417  sbcrexgOLD  35699  sbcel12gOLD  36975  2sb5nd  36997  2sb5ndALT  37392  opeliun2xp  40622