Theorem nfs1v 2233

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

Syntax hints:   F/wnf 1664   [wsb 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-12 1906  ax-13 2054

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788

This theorem is referenced by:  mo3  2304  eu1  2307  2mo  2348  2moOLD  2349  2eu6  2357  clelabOLD  2568  cbvralf  3050  cbvralsv  3067  cbvrexsv  3068  cbvrab  3080  sbhypf  3129  mob2  3252  reu2  3260  reu2eqd  3269  sbcralt  3373  sbcreu  3377  cbvreucsf  3430  cbvrabcsf  3431  sbcel12  3801  sbceqg  3802  csbif  3960  rabasiun  4301  cbvopab1  4492  cbvopab1s  4494  cbvmptf  4512  cbvmpt  4513  opelopabsb  4728  csbopab  4750  csbopabgALT  4751  opeliunxp  4903  ralxpf  4998  cbviota  5568  csbiota  5592  isarep1  5678  cbvriota  6275  csbriota  6277  onminex  6646  tfis  6693  findes  6735  abrexex2g  6782  abrexex2  6786  dfoprab4f  6863  axrepndlem1  9019  axrepndlem2  9020  uzind4s  11221  mo5f  28112  ac6sf2  28222  esumcvg  28909  bj-mo3OLD  31411  wl-lem-moexsb  31855  wl-mo3t  31863  poimirlem26  31924  sbcalf  32310  sbcexf  32311  sbcrexgOLD  35591  sbcel12gOLD  36807  2sb5nd  36829  2sb5ndALT  37234  opeliun2xp  39458