Theorem nfs1v 1856

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 1855	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nfi 1391	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1389  [wsb 1685

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686

This theorem is referenced by:  nfsbxy  1859  nfsbxyt  1860  sbco3v  1884  sbcomxyyz  1887  sbnf2  1898  mo2n  1969  mo23  1982  mor  1983  clelab  2203  cbvralf  2571  cbvrexf  2572  cbvralsv  2588  cbvrexsv  2589  cbvrab  2599  sbhypf  2648  mob2  2772  reu2  2780  sbcralt  2890  sbcrext  2891  sbcralg  2892  sbcreug  2894  sbcel12g  2921  sbceqg  2922  cbvreucsf  2966  cbvrabcsf  2967  cbvopab1  3851  cbvopab1s  3853  csbopabg  3856  cbvmpt  3872  opelopabsb  4015  frind  4107  tfis  4324  findes  4344  opeliunxp  4413  ralxpf  4500  rexxpf  4501  cbviota  4892  csbiotag  4915  isarep1  5005  cbvriota  5498  csbriotag  5500  abrexex2g  5767  abrexex2  5771  dfoprab4f  5839  uzind4s  8678  zsupcllemstep  10341  bezoutlemmain  10387  cbvrald  10598  bj-bdfindes  10744  bj-findes  10776