MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfs1v Structured version   Unicode version

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
StepHypRef Expression
1 hbs1 2181 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1560 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1553   [wsb 1658
This theorem is referenced by:  sbnf2  2184  eu1  2302  mo  2303  mopick  2343  2mo  2359  2eu6  2366  clelab  2556  cbvralf  2926  cbvralsv  2943  cbvrexsv  2944  cbvrab  2954  sbhypf  3001  mob2  3114  reu2  3122  sbcralt  3233  sbcralg  3235  sbcrexg  3236  sbcreug  3237  sbcel12g  3266  sbceqg  3267  cbvreucsf  3313  cbvrabcsf  3314  csbifg  3767  cbvopab1  4278  cbvopab1s  4280  csbopabg  4283  cbvmpt  4299  opelopabsb  4465  onminex  4787  tfis  4834  findes  4875  opeliunxp  4929  ralxpf  5019  cbviota  5423  csbiotag  5447  isarep1  5532  abrexex2g  5988  abrexex2  6001  dfoprab4f  6405  cbvriota  6560  csbriotag  6562  axrepndlem1  8467  axrepndlem2  8468  uzind4s  10536  mo5f  23972  cbvmptf  24068  esumcvg  24476  2sb5nd  28647  2sb5ndALT  29044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659
  Copyright terms: Public domain W3C validator