Theorem nfs1v 1870

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

Syntax hints:  Ⅎwnf 1401  [wsb 1699

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700

This theorem is referenced by:  nfsbxy  1873  nfsbxyt  1874  sbco3v  1898  sbcomxyyz  1901  sbnf2  1912  mo2n  1983  mo23  1996  mor  1997  clelab  2219  cbvralf  2598  cbvrexf  2599  cbvralsv  2615  cbvrexsv  2616  cbvrab  2631  sbhypf  2682  mob2  2809  reu2  2817  sbcralt  2929  sbcrext  2930  sbcralg  2931  sbcreug  2933  sbcel12g  2960  sbceqg  2961  cbvreucsf  3006  cbvrabcsf  3007  disjiun  3862  cbvopab1  3933  cbvopab1s  3935  csbopabg  3938  cbvmptf  3954  cbvmpt  3955  opelopabsb  4111  frind  4203  tfis  4426  findes  4446  opeliunxp  4522  ralxpf  4613  rexxpf  4614  cbviota  5019  csbiotag  5042  isarep1  5134  cbvriota  5656  csbriotag  5658  abrexex2g  5929  abrexex2  5933  dfoprab4f  6001  finexdc  6698  ssfirab  6723  uzind4s  9177  zsupcllemstep  11368  bezoutlemmain  11414  cbvrald  12405  bj-bdfindes  12561  bj-findes  12593