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

Theorem nfs1v 2045
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 2044 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1538 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1531   [wsb 1629
This theorem is referenced by:  sbnf2  2047  eu1  2164  mopick  2205  2mo  2221  2eu6  2228  clelab  2403  cbvralf  2758  cbvralsv  2775  cbvrexsv  2776  cbvrab  2786  sbhypf  2833  mob2  2945  reu2  2953  sbcralt  3063  sbcralg  3065  sbcrexg  3066  sbcreug  3067  sbcel12g  3096  sbceqg  3097  cbvreucsf  3145  cbvrabcsf  3146  csbifg  3593  cbvopab1  4089  cbvopab1s  4091  csbopabg  4094  cbvmpt  4110  opelopabsb  4275  onminex  4598  tfis  4645  findes  4686  opeliunxp  4740  ralxpf  4830  cbviota  5224  csbiotag  5248  isarep1  5331  abrexex2g  5768  abrexex2  5780  dfoprab4f  6178  cbvriota  6315  csbriotag  6317  axrepndlem1  8214  axrepndlem2  8215  uzind4s  10278  cbvmptf  23220  esumcvg  23454  2sb5nd  28326  2sb5ndALT  28709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630
  Copyright terms: Public domain W3C validator