Theorem nfs1v 2142

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

Syntax hints:   F/wnf 1589   [wsb 1700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701

This theorem is referenced by:  sbnf2OLD  2145  mo3  2298  mo3OLD  2299  eu1  2303  eu1OLD  2304  moOLD  2305  mopickOLDOLD  2341  2mo  2360  2moOLD  2361  2moOLDOLD  2362  2eu6  2371  2eu6OLD  2372  clelab  2563  cbvralf  2941  cbvralsv  2958  cbvrexsv  2959  cbvrab  2970  sbhypf  3019  mob2  3139  reu2  3147  sbcralt  3267  sbcrexgOLD  3272  sbcreu  3273  sbcreugOLD  3274  cbvreucsf  3321  cbvrabcsf  3322  sbcel12  3675  sbcel12gOLD  3676  sbceqg  3677  csbif  3839  csbifgOLD  3840  cbvopab1  4362  cbvopab1s  4364  cbvmpt  4382  opelopabsb  4599  csbopab  4620  csbopabgALT  4621  opeliunxp  4890  ralxpf  4986  cbviota  5386  csbiota  5410  csbiotagOLD  5411  isarep1  5497  cbvriota  6062  csbriota  6064  onminex  6418  tfis  6465  findes  6506  abrexex2g  6554  abrexex2  6558  dfoprab4f  6632  axrepndlem1  8756  axrepndlem2  8757  uzind4s  10914  mo5f  25868  cbvmptf  25971  esumcvg  26535  wl-lem-moexsb  28393  wl-mo3t  28397  sbcalf  28920  sbcexf  28921  rabasiun  30230  opeliun2xp  30720  2sb5nd  31269  2sb5ndALT  31668