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  10505  axrepndlem2  10506  uzind4s  12823  mo5f  32565  ac6sf2  32702  esumcvg  34245  bj-gabima  37143  wl-lem-moexsb  37775  wl-mo3t  37783  poimirlem26  37849  sbcalf  38317  sbcexf  38318  sbcrexgOLD  43048  scottabes  44504  2sb5nd  44822  2sb5ndALT  45193  2reu8i  47380  dfich2  47725