Theorem nfs1v 2425

Description: The setvar 𝑥 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 2424	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nf5i 2011	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1699  [wsb 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868

This theorem is referenced by:  mo3  2495  eu1  2498  2mo  2539  2eu6  2546  cbvralf  3141  cbvralsv  3158  cbvrexsv  3159  cbvrab  3171  sbhypf  3226  mob2  3353  reu2  3361  reu2eqd  3370  sbcralt  3477  sbcreu  3482  cbvreucsf  3533  cbvrabcsf  3534  sbcel12  3935  sbceqg  3936  csbif  4088  rabasiun  4459  cbvopab1  4655  cbvopab1s  4657  cbvmptf  4676  cbvmpt  4677  opelopabsb  4910  csbopab  4932  csbopabgALT  4933  opeliunxp  5093  ralxpf  5190  cbviota  5773  csbiota  5797  isarep1  5891  cbvriota  6521  csbriota  6523  onminex  6899  tfis  6946  findes  6988  abrexex2g  7036  abrexex2  7040  dfoprab4f  7117  axrepndlem1  9293  axrepndlem2  9294  uzind4s  11624  mo5f  28708  ac6sf2  28810  esumcvg  29475  bj-mo3OLD  32022  wl-lem-moexsb  32529  wl-mo3t  32537  poimirlem26  32605  sbcalf  33087  sbcexf  33088  sbcrexgOLD  36367  sbcel12gOLD  37775  2sb5nd  37797  2sb5ndALT  38190  opeliun2xp  41904