Theorem nfs1v 1912

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

Syntax hints:  Ⅎwnf 1436  [wsb 1735

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736

This theorem is referenced by:  nfsbxy  1915  nfsbxyt  1916  sbco3v  1942  sbcomxyyz  1945  sbnf2  1956  mo2n  2027  mo23  2040  mor  2041  clelab  2265  cbvralf  2648  cbvrexf  2649  cbvralsv  2668  cbvrexsv  2669  cbvrab  2684  sbhypf  2735  mob2  2864  reu2  2872  sbcralt  2985  sbcrext  2986  sbcralg  2987  sbcreug  2989  sbcel12g  3017  sbceqg  3018  cbvreucsf  3064  cbvrabcsf  3065  disjiun  3924  cbvopab1  4001  cbvopab1s  4003  csbopabg  4006  cbvmptf  4022  cbvmpt  4023  opelopabsb  4182  frind  4274  tfis  4497  findes  4517  opeliunxp  4594  ralxpf  4685  rexxpf  4686  cbviota  5093  csbiotag  5116  isarep1  5209  cbvriota  5740  csbriotag  5742  abrexex2g  6018  abrexex2  6022  dfoprab4f  6091  finexdc  6796  ssfirab  6822  uzind4s  9385  zsupcllemstep  11638  bezoutlemmain  11686  cbvrald  12995  bj-bdfindes  13147  bj-findes  13179