Theorem nfs1v 2182

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

Syntax hints:   F/wnf 1617   [wsb 1740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855  ax-13 2000

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-nf 1618  df-sb 1741

This theorem is referenced by:  mo3  2324  mo3OLD  2325  eu1  2328  2mo  2373  2moOLD  2374  2eu6  2383  2eu6OLD  2384  clelabOLD  2602  cbvralf  3078  cbvralsv  3095  cbvrexsv  3096  cbvrab  3107  sbhypf  3156  mob2  3279  reu2  3287  reu2eqd  3296  sbcralt  3406  sbcrexgOLD  3410  sbcreu  3411  cbvreucsf  3464  cbvrabcsf  3465  sbcel12  3832  sbcel12gOLD  3833  sbceqg  3834  csbif  3994  csbifgOLD  3995  rabasiun  4336  cbvopab1  4527  cbvopab1s  4529  cbvmpt  4547  opelopabsb  4766  csbopab  4788  csbopabgALT  4789  opeliunxp  5060  ralxpf  5159  cbviota  5562  csbiota  5586  csbiotagOLD  5587  isarep1  5673  cbvriota  6268  csbriota  6270  onminex  6641  tfis  6688  findes  6729  abrexex2g  6776  abrexex2  6780  dfoprab4f  6857  axrepndlem1  8984  axrepndlem2  8985  uzind4s  11166  mo5f  27509  ac6sf2  27610  cbvmptf  27637  esumcvg  28248  wl-lem-moexsb  30179  wl-mo3t  30183  sbcalf  30679  sbcexf  30680  opeliun2xp  33024  2sb5nd  33434  2sb5ndALT  33833