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

Theorem nfs1v 1831
Description: 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfs1v 𝑥[𝑦 / 𝑥]𝜑
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfs1v
StepHypRef Expression
1 hbs1 1830 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
21nfi 1367 1 𝑥[𝑦 / 𝑥]𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1365  [wsb 1661
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662
This theorem is referenced by:  nfsbxy  1834  nfsbxyt  1835  sbco3v  1859  sbcomxyyz  1862  sbnf2  1873  mo2n  1944  mo23  1957  mor  1958  clelab  2178  cbvralf  2544  cbvrexf  2545  cbvralsv  2561  cbvrexsv  2562  cbvrab  2572  sbhypf  2620  mob2  2744  reu2  2752  sbcralt  2862  sbcrext  2863  sbcralg  2864  sbcreug  2866  sbcel12g  2893  sbceqg  2894  cbvreucsf  2938  cbvrabcsf  2939  cbvopab1  3858  cbvopab1s  3860  csbopabg  3863  cbvmpt  3879  opelopabsb  4025  frind  4117  tfis  4334  findes  4354  opeliunxp  4423  ralxpf  4510  rexxpf  4511  cbviota  4900  csbiotag  4923  isarep1  5013  cbvriota  5506  csbriotag  5508  abrexex2g  5775  abrexex2  5779  dfoprab4f  5847  uzind4s  8629  cbvrald  10314  bj-bdfindes  10461  bj-findes  10493
  Copyright terms: Public domain W3C validator