Theorem nfs1v 1995

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

Syntax hints:  Ⅎwnf 1509  [wsb 1811

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  nfsbxy  1998  nfsbxyt  1999  sbco3v  2025  sbcomxyyz  2028  sbnf2  2037  mo2n  2110  mo23  2124  mor  2125  clelab  2362  cbvralf  2771  cbvrexf  2772  cbvralsv  2796  cbvrexsv  2797  cbvrab  2813  sbhypf  2866  mob2  3000  reu2  3008  sbcralt  3122  sbcrext  3123  sbcralg  3124  sbcreug  3126  sbcel12g  3156  sbceqg  3157  cbvreucsf  3206  cbvrabcsf  3207  disjiun  4109  cbvopab1  4188  cbvopab1s  4190  csbopabg  4193  cbvmptf  4209  cbvmpt  4210  opelopabsb  4383  frind  4478  tfis  4710  findes  4730  opeliunxp  4810  ralxpf  4906  rexxpf  4907  cbviota  5322  csbiotag  5350  isarep1  5447  cbvriota  6023  csbriotag  6025  abrexex2g  6322  abrexex2  6326  dfoprab4f  6400  modom  7074  finexdc  7173  ssfirab  7210  uzind4s  9940  zsupcllemstep  10611  bezoutlemmain  12719  nnwosdc  12760  cbvrald  16686  bj-bdfindes  16845  bj-findes  16877