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

Theorem nfs1v 2058
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 2057 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1541 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1534   [wsb 1638
This theorem is referenced by:  sbnf2  2060  eu1  2177  mopick  2218  2mo  2234  2eu6  2241  clelab  2416  cbvralf  2771  cbvralsv  2788  cbvrexsv  2789  cbvrab  2799  sbhypf  2846  mob2  2958  reu2  2966  sbcralt  3076  sbcralg  3078  sbcrexg  3079  sbcreug  3080  sbcel12g  3109  sbceqg  3110  cbvreucsf  3158  cbvrabcsf  3159  csbifg  3606  cbvopab1  4105  cbvopab1s  4107  csbopabg  4110  cbvmpt  4126  opelopabsb  4291  onminex  4614  tfis  4661  findes  4702  opeliunxp  4756  ralxpf  4846  cbviota  5240  csbiotag  5264  isarep1  5347  abrexex2g  5784  abrexex2  5796  dfoprab4f  6194  cbvriota  6331  csbriotag  6333  axrepndlem1  8230  axrepndlem2  8231  uzind4s  10294  cbvmptf  23235  esumcvg  23469  itgaddnclem2  25010  2sb5nd  28625  2sb5ndALT  29025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639
  Copyright terms: Public domain W3C validator