Theorem nfs1v 2437

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 2436	. 2 ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
2	1	nf5i 2024	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:  Ⅎwnf 1708  [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  mo3  2507  eu1  2510  2mo  2551  2eu6  2558  cbvralf  3165  cbvralsv  3182  cbvrexsv  3183  cbvrab  3198  sbhypf  3253  mob2  3386  reu2  3394  reu2eqd  3403  sbcralt  3510  sbcreu  3515  cbvreucsf  3567  cbvrabcsf  3568  sbcel12  3983  sbceqg  3984  csbif  4138  cbvopab1  4723  cbvopab1s  4725  cbvmptf  4748  cbvmpt  4749  opelopabsb  4985  csbopab  5008  csbopabgALT  5009  opeliunxp  5170  ralxpf  5268  cbviota  5856  csbiota  5881  isarep1  5977  cbvriota  6621  csbriota  6623  onminex  7007  tfis  7054  findes  7096  abrexex2g  7144  abrexex2OLD  7150  dfoprab4f  7226  axrepndlem1  9414  axrepndlem2  9415  uzind4s  11748  mo5f  29324  ac6sf2  29429  esumcvg  30148  bj-mo3OLD  32832  wl-lem-moexsb  33350  wl-mo3t  33358  poimirlem26  33435  sbcalf  33917  sbcexf  33918  sbcrexgOLD  37349  sbcel12gOLD  38754  2sb5nd  38776  2sb5ndALT  39168  opeliun2xp  42111