Theorem nfs1v 1932

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

Syntax hints:  Ⅎwnf 1453  [wsb 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756

This theorem is referenced by:  nfsbxy  1935  nfsbxyt  1936  sbco3v  1962  sbcomxyyz  1965  sbnf2  1974  mo2n  2047  mo23  2060  mor  2061  clelab  2296  cbvralf  2689  cbvrexf  2690  cbvralsv  2712  cbvrexsv  2713  cbvrab  2728  sbhypf  2779  mob2  2910  reu2  2918  sbcralt  3031  sbcrext  3032  sbcralg  3033  sbcreug  3035  sbcel12g  3064  sbceqg  3065  cbvreucsf  3113  cbvrabcsf  3114  disjiun  3984  cbvopab1  4062  cbvopab1s  4064  csbopabg  4067  cbvmptf  4083  cbvmpt  4084  opelopabsb  4245  frind  4337  tfis  4567  findes  4587  opeliunxp  4666  ralxpf  4757  rexxpf  4758  cbviota  5165  csbiotag  5191  isarep1  5284  cbvriota  5819  csbriotag  5821  abrexex2g  6099  abrexex2  6103  dfoprab4f  6172  finexdc  6880  ssfirab  6911  uzind4s  9549  zsupcllemstep  11900  bezoutlemmain  11953  nnwosdc  11994  cbvrald  13823  bj-bdfindes  13984  bj-findes  14016