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

Theorem nfsb 1899
Description: If  z is not free in  ph, it is not free in  [ y  /  x ] ph when  y and  z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
Hypothesis
Ref Expression
nfsb.1  |-  F/ z
ph
Assertion
Ref Expression
nfsb  |-  F/ z [ y  /  x ] ph
Distinct variable group:    y, z
Allowed substitution hints:    ph( x, y, z)

Proof of Theorem nfsb
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 nfsb.1 . . . 4  |-  F/ z
ph
21nfsbxy 1895 . . 3  |-  F/ z [ w  /  x ] ph
32nfsbxy 1895 . 2  |-  F/ z [ y  /  w ] [ w  /  x ] ph
4 ax-17 1491 . . . 4  |-  ( ph  ->  A. w ph )
54sbco2v 1898 . . 3  |-  ( [ y  /  w ] [ w  /  x ] ph  <->  [ y  /  x ] ph )
65nfbii 1434 . 2  |-  ( F/ z [ y  /  w ] [ w  /  x ] ph  <->  F/ z [ y  /  x ] ph )
73, 6mpbi 144 1  |-  F/ z [ 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-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721
This theorem is referenced by:  hbsb  1900  sbco2yz  1914  sbcomxyyz  1923  hbsbd  1935  nfsb4or  1976  sb8eu  1990  nfeu  1996  cbvab  2240  cbvralf  2625  cbvrexf  2626  cbvreu  2629  cbvralsv  2642  cbvrexsv  2643  cbvrab  2658  cbvreucsf  3034  cbvrabcsf  3035  cbvopab1  3971  cbvmptf  3992  cbvmpt  3993  ralxpf  4655  rexxpf  4656  cbviota  5063  sb8iota  5065  cbvriota  5708  dfoprab4f  6059
  Copyright terms: Public domain W3C validator