Theorem nfs1v 1992

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

Step	Hyp	Ref	Expression
1		hbs1 1991	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nfi 1510	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1508  [wsb 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811

This theorem is referenced by:  nfsbxy  1995  nfsbxyt  1996  sbco3v  2022  sbcomxyyz  2025  sbnf2  2034  mo2n  2107  mo23  2121  mor  2122  clelab  2357  cbvralf  2758  cbvrexf  2759  cbvralsv  2783  cbvrexsv  2784  cbvrab  2800  sbhypf  2853  mob2  2986  reu2  2994  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcreug  3112  sbcel12g  3142  sbceqg  3143  cbvreucsf  3192  cbvrabcsf  3193  disjiun  4083  cbvopab1  4162  cbvopab1s  4164  csbopabg  4167  cbvmptf  4183  cbvmpt  4184  opelopabsb  4354  frind  4449  tfis  4681  findes  4701  opeliunxp  4781  ralxpf  4876  rexxpf  4877  cbviota  5291  csbiotag  5319  isarep1  5416  cbvriota  5983  csbriotag  5985  abrexex2g  6282  abrexex2  6286  dfoprab4f  6356  modom  6994  finexdc  7092  ssfirab  7129  uzind4s  9824  zsupcllemstep  10490  bezoutlemmain  12574  nnwosdc  12615  cbvrald  16410  bj-bdfindes  16570  bj-findes  16602