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

Theorem nfs1v 1890
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 1889 . 2  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
21nfi 1421 1  |-  F/ x [ y  /  x ] ph
Colors of variables: wff set class
Syntax hints:   F/wnf 1419   [wsb 1718
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719
This theorem is referenced by:  nfsbxy  1893  nfsbxyt  1894  sbco3v  1918  sbcomxyyz  1921  sbnf2  1932  mo2n  2003  mo23  2016  mor  2017  clelab  2240  cbvralf  2623  cbvrexf  2624  cbvralsv  2640  cbvrexsv  2641  cbvrab  2656  sbhypf  2707  mob2  2835  reu2  2843  sbcralt  2955  sbcrext  2956  sbcralg  2957  sbcreug  2959  sbcel12g  2986  sbceqg  2987  cbvreucsf  3032  cbvrabcsf  3033  disjiun  3892  cbvopab1  3969  cbvopab1s  3971  csbopabg  3974  cbvmptf  3990  cbvmpt  3991  opelopabsb  4150  frind  4242  tfis  4465  findes  4485  opeliunxp  4562  ralxpf  4653  rexxpf  4654  cbviota  5061  csbiotag  5084  isarep1  5177  cbvriota  5706  csbriotag  5708  abrexex2g  5984  abrexex2  5988  dfoprab4f  6057  finexdc  6762  ssfirab  6788  uzind4s  9337  zsupcllemstep  11545  bezoutlemmain  11593  cbvrald  12829  bj-bdfindes  12981  bj-findes  13013
  Copyright terms: Public domain W3C validator