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

Theorem nfs1v 2183
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 2182 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1561 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1554   [wsb 1659
This theorem is referenced by:  sbnf2  2185  eu1  2303  mo  2304  mopick  2344  2mo  2360  2eu6  2367  clelab  2557  cbvralf  2927  cbvralsv  2944  cbvrexsv  2945  cbvrab  2955  sbhypf  3002  mob2  3115  reu2  3123  sbcralt  3234  sbcralg  3236  sbcrexg  3237  sbcreug  3238  sbcel12g  3267  sbceqg  3268  cbvreucsf  3314  cbvrabcsf  3315  csbifg  3768  cbvopab1  4279  cbvopab1s  4281  csbopabg  4284  cbvmpt  4300  opelopabsb  4466  onminex  4788  tfis  4835  findes  4876  opeliunxp  4930  ralxpf  5020  cbviota  5424  csbiotag  5448  isarep1  5533  abrexex2g  5989  abrexex2  6002  dfoprab4f  6406  cbvriota  6561  csbriotag  6563  axrepndlem1  8468  axrepndlem2  8469  uzind4s  10537  mo5f  23973  cbvmptf  24069  esumcvg  24477  2sb5nd  28648  2sb5ndALT  29045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660
  Copyright terms: Public domain W3C validator