Theorem nfs1v 2193

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2193 and hbs1 2307 combined. (Revised by Wolf Lammen, 28-Jul-2022.)

Assertion

Ref	Expression
nfs1v	⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)

Proof of Theorem nfs1v

Step	Hyp	Ref	Expression
1		sb6 2122	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2188	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1886	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100

This theorem is used by:  hbs1  2307  sb8ef  2384  sbbib  2390  sb2ae  2525  mo3  2589  eu1  2635  2mo  2673  2eu6  2681  nfsab1  2746  cbvrexsvw  3314  cbvralf  3345  cbvralsv  3351  cbvrexsv  3352  cbvrab  3449  mob2  3673  reu2  3683  reu2eqd  3694  sbcralt  3819  sbcreu  3823  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  sbcel12  4369  sbceqg  4370  2nreu  4402  csbif  4540  rexreusng  4640  cbvopab1  5179  cbvopab1g  5180  cbvopab1s  5182  cbvmptf  5205  cbvmptfg  5206  csbopab  5534  csbopabw  5535  opeliunxp  5722  opeliun2xp  5723  ralxpf  5826  cbviotaw  6496  cbviota  6498  csbiota  6526  isarep1  6622  f1ossf1o  7123  cbvriotaw  7380  cbvriota  7384  csbriota  7386  onminex  7802  tfis  7852  findes  7898  abrexex2g  7962  dfoprab4f  8054  scottabes  9883  axrepndlem1  10604  axrepndlem2  10605  uzind4s  12960  mo5f  32967  ac6sf2  33098  esumcvg  34599  bj-gabima  37687  wl-lem-moexsb  38334  wl-mo3t  38342  poimirlem26  38398  sbcalf  38865  sbcexf  38866  2sb5nd  45386  2sb5ndALT  45757  2reu8i  48004  dfich2  48361