Theorem nfs1v 2161

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2161 and hbs1 2280 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 2090	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2156	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1854	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068

This theorem is referenced by:  hbs1  2280  sb8ef  2359  sbbib  2365  sb2ae  2500  mo3  2564  eu1  2610  2mo  2648  2eu6  2657  nfsab1  2722  cbvrexsvw  3288  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbvrexsvwOLD  3291  cbvralf  3330  cbvralsv  3336  cbvrexsv  3337  cbvrabwOLD  3435  cbvrab  3439  mob2  3673  reu2  3683  reu2eqd  3694  sbcralt  3822  sbcreu  3826  cbvrabcsfw  3890  cbvreucsf  3893  cbvrabcsf  3894  sbcel12  4363  sbceqg  4364  2nreu  4396  csbif  4537  rexreusng  4636  cbvopab1  5172  cbvopab1g  5173  cbvopab1s  5175  cbvmptf  5198  cbvmptfg  5199  csbopab  5503  csbopabgALT  5504  opeliunxp  5691  opeliun2xp  5692  ralxpf  5795  cbviotaw  6455  cbviota  6457  csbiota  6485  isarep1  6581  f1ossf1o  7073  cbvriotaw  7324  cbvriota  7328  csbriota  7330  onminex  7747  tfis  7797  findes  7842  abrexex2g  7908  dfoprab4f  8000  axrepndlem1  10503  axrepndlem2  10504  uzind4s  12821  mo5f  32563  ac6sf2  32700  esumcvg  34243  bj-gabima  37141  wl-lem-moexsb  37773  wl-mo3t  37781  poimirlem26  37847  sbcalf  38315  sbcexf  38316  sbcrexgOLD  43027  scottabes  44483  2sb5nd  44801  2sb5ndALT  45172  2reu8i  47359  dfich2  47704