Theorem nfs1v 1949

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

Syntax hints:  Ⅎwnf 1470  [wsb 1772

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773

This theorem is referenced by:  nfsbxy  1952  nfsbxyt  1953  sbco3v  1979  sbcomxyyz  1982  sbnf2  1991  mo2n  2064  mo23  2077  mor  2078  clelab  2313  cbvralf  2707  cbvrexf  2708  cbvralsv  2731  cbvrexsv  2732  cbvrab  2747  sbhypf  2798  mob2  2929  reu2  2937  sbcralt  3051  sbcrext  3052  sbcralg  3053  sbcreug  3055  sbcel12g  3084  sbceqg  3085  cbvreucsf  3133  cbvrabcsf  3134  disjiun  4010  cbvopab1  4088  cbvopab1s  4090  csbopabg  4093  cbvmptf  4109  cbvmpt  4110  opelopabsb  4272  frind  4364  tfis  4594  findes  4614  opeliunxp  4693  ralxpf  4785  rexxpf  4786  cbviota  5195  csbiotag  5221  isarep1  5314  cbvriota  5854  csbriotag  5856  abrexex2g  6134  abrexex2  6138  dfoprab4f  6207  finexdc  6915  ssfirab  6946  uzind4s  9603  zsupcllemstep  11959  bezoutlemmain  12012  nnwosdc  12053  cbvrald  14811  bj-bdfindes  14972  bj-findes  15004