Theorem nfs1v 1990

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

Syntax hints:  Ⅎwnf 1506  [wsb 1808

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809

This theorem is referenced by:  nfsbxy  1993  nfsbxyt  1994  sbco3v  2020  sbcomxyyz  2023  sbnf2  2032  mo2n  2105  mo23  2119  mor  2120  clelab  2355  cbvralf  2756  cbvrexf  2757  cbvralsv  2781  cbvrexsv  2782  cbvrab  2797  sbhypf  2850  mob2  2983  reu2  2991  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcreug  3109  sbcel12g  3139  sbceqg  3140  cbvreucsf  3189  cbvrabcsf  3190  disjiun  4077  cbvopab1  4156  cbvopab1s  4158  csbopabg  4161  cbvmptf  4177  cbvmpt  4178  opelopabsb  4347  frind  4442  tfis  4674  findes  4694  opeliunxp  4773  ralxpf  4867  rexxpf  4868  cbviota  5282  csbiotag  5310  isarep1  5406  cbvriota  5965  csbriotag  5967  abrexex2g  6263  abrexex2  6267  dfoprab4f  6337  finexdc  7060  ssfirab  7094  uzind4s  9781  zsupcllemstep  10444  bezoutlemmain  12514  nnwosdc  12555  cbvrald  16110  bj-bdfindes  16270  bj-findes  16302