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  2798  sbhypf  2851  mob2  2984  reu2  2992  sbcralt  3106  sbcrext  3107  sbcralg  3108  sbcreug  3110  sbcel12g  3140  sbceqg  3141  cbvreucsf  3190  cbvrabcsf  3191  disjiun  4081  cbvopab1  4160  cbvopab1s  4162  csbopabg  4165  cbvmptf  4181  cbvmpt  4182  opelopabsb  4352  frind  4447  tfis  4679  findes  4699  opeliunxp  4779  ralxpf  4874  rexxpf  4875  cbviota  5289  csbiotag  5317  isarep1  5413  cbvriota  5978  csbriotag  5980  abrexex2g  6277  abrexex2  6281  dfoprab4f  6351  modom  6989  finexdc  7085  ssfirab  7121  uzind4s  9814  zsupcllemstep  10479  bezoutlemmain  12559  nnwosdc  12600  cbvrald  16320  bj-bdfindes  16480  bj-findes  16512