Theorem nfs1v 2164

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

Syntax hints:   F/wnf 1599   [wsb 1711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712

This theorem is referenced by:  sbnf2OLD  2167  mo3  2320  mo3OLD  2321  eu1  2325  eu1OLD  2326  moOLD  2327  mopickOLDOLD  2363  2mo  2382  2moOLD  2383  2moOLDOLD  2384  2eu6  2393  2eu6OLD  2394  clelabOLD  2612  cbvralf  3082  cbvralsv  3099  cbvrexsv  3100  cbvrab  3111  sbhypf  3160  mob2  3283  reu2  3291  reu2eqd  3300  sbcralt  3412  sbcrexgOLD  3417  sbcreu  3418  sbcreugOLD  3419  cbvreucsf  3469  cbvrabcsf  3470  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbif  3989  csbifgOLD  3990  rabasiun  4329  cbvopab1  4517  cbvopab1s  4519  cbvmpt  4537  opelopabsb  4757  csbopab  4779  csbopabgALT  4780  opeliunxp  5051  ralxpf  5149  cbviota  5556  csbiota  5580  csbiotagOLD  5581  isarep1  5667  cbvriota  6255  csbriota  6257  onminex  6626  tfis  6673  findes  6714  abrexex2g  6761  abrexex2  6765  dfoprab4f  6842  axrepndlem1  8967  axrepndlem2  8968  uzind4s  11141  mo5f  27087  cbvmptf  27194  esumcvg  27760  wl-lem-moexsb  29622  wl-mo3t  29626  sbcalf  30148  sbcexf  30149  opeliun2xp  32018  2sb5nd  32431  2sb5ndALT  32830