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

Theorem nfs1v 2142
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 2141 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1596 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1589   [wsb 1700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701
This theorem is referenced by:  sbnf2OLD  2145  mo3  2298  mo3OLD  2299  eu1  2303  eu1OLD  2304  moOLD  2305  mopickOLDOLD  2341  2mo  2360  2moOLD  2361  2moOLDOLD  2362  2eu6  2371  2eu6OLD  2372  clelab  2563  cbvralf  2941  cbvralsv  2958  cbvrexsv  2959  cbvrab  2970  sbhypf  3019  mob2  3139  reu2  3147  sbcralt  3267  sbcrexgOLD  3272  sbcreu  3273  sbcreugOLD  3274  cbvreucsf  3321  cbvrabcsf  3322  sbcel12  3675  sbcel12gOLD  3676  sbceqg  3677  csbif  3839  csbifgOLD  3840  cbvopab1  4362  cbvopab1s  4364  cbvmpt  4382  opelopabsb  4599  csbopab  4620  csbopabgALT  4621  opeliunxp  4890  ralxpf  4986  cbviota  5386  csbiota  5410  csbiotagOLD  5411  isarep1  5497  cbvriota  6062  csbriota  6064  onminex  6418  tfis  6465  findes  6506  abrexex2g  6554  abrexex2  6558  dfoprab4f  6632  axrepndlem1  8756  axrepndlem2  8757  uzind4s  10914  mo5f  25868  cbvmptf  25971  esumcvg  26535  wl-lem-moexsb  28393  wl-mo3t  28397  sbcalf  28920  sbcexf  28921  rabasiun  30230  opeliun2xp  30720  2sb5nd  31269  2sb5ndALT  31668
  Copyright terms: Public domain W3C validator