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

Theorem nfs1v 1863
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 1862 . 2 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
21nfi 1396 1 𝑥[𝑦 / 𝑥]𝜑
Colors of variables: wff set class
Syntax hints:  wnf 1394  [wsb 1692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693
This theorem is referenced by:  nfsbxy  1866  nfsbxyt  1867  sbco3v  1891  sbcomxyyz  1894  sbnf2  1905  mo2n  1976  mo23  1989  mor  1990  clelab  2212  cbvralf  2584  cbvrexf  2585  cbvralsv  2601  cbvrexsv  2602  cbvrab  2617  sbhypf  2668  mob2  2793  reu2  2801  sbcralt  2913  sbcrext  2914  sbcralg  2915  sbcreug  2917  sbcel12g  2944  sbceqg  2945  cbvreucsf  2990  cbvrabcsf  2991  disjiun  3832  cbvopab1  3903  cbvopab1s  3905  csbopabg  3908  cbvmptf  3924  cbvmpt  3925  opelopabsb  4078  frind  4170  tfis  4388  findes  4408  opeliunxp  4481  ralxpf  4570  rexxpf  4571  cbviota  4972  csbiotag  4995  isarep1  5086  cbvriota  5600  csbriotag  5602  abrexex2g  5873  abrexex2  5877  dfoprab4f  5945  finexdc  6598  ssfirab  6622  uzind4s  9047  zsupcllemstep  11023  bezoutlemmain  11069  cbvrald  11334  bj-bdfindes  11490  bj-findes  11522
  Copyright terms: Public domain W3C validator