ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfs1v Unicode version

Theorem nfs1v 1892
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 1891 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1423 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1421   [wsb 1720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721
This theorem is referenced by:  nfsbxy  1895  nfsbxyt  1896  sbco3v  1920  sbcomxyyz  1923  sbnf2  1934  mo2n  2005  mo23  2018  mor  2019  clelab  2242  cbvralf  2625  cbvrexf  2626  cbvralsv  2642  cbvrexsv  2643  cbvrab  2658  sbhypf  2709  mob2  2837  reu2  2845  sbcralt  2957  sbcrext  2958  sbcralg  2959  sbcreug  2961  sbcel12g  2988  sbceqg  2989  cbvreucsf  3034  cbvrabcsf  3035  disjiun  3894  cbvopab1  3971  cbvopab1s  3973  csbopabg  3976  cbvmptf  3992  cbvmpt  3993  opelopabsb  4152  frind  4244  tfis  4467  findes  4487  opeliunxp  4564  ralxpf  4655  rexxpf  4656  cbviota  5063  csbiotag  5086  isarep1  5179  cbvriota  5708  csbriotag  5710  abrexex2g  5986  abrexex2  5990  dfoprab4f  6059  finexdc  6764  ssfirab  6790  uzind4s  9353  zsupcllemstep  11565  bezoutlemmain  11613  cbvrald  12922  bj-bdfindes  13074  bj-findes  13106
  Copyright terms: Public domain W3C validator