Theorem nfs1v 2146

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

Syntax hints:   → wi 4  ∀wal 1532  Ⅎwnf 1778  [wsb 2060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-nf 1779  df-sb 2061

This theorem is referenced by:  hbs1  2258  sb5OLD  2261  sb8fOLD  2345  sb8ef  2346  sbbib  2352  sb2ae  2490  mo3  2553  eu1  2601  2mo  2639  2eu6  2647  nfsab1  2712  cbvralsvw  3309  cbvrexsvw  3310  cbvralsvwOLD  3311  cbvrexsvwOLD  3312  cbvralfwOLD  3315  cbvralf  3351  cbvralsv  3357  cbvrexsv  3358  cbvrabw  3462  cbvrab  3468  sbhypfOLD  3535  mob2  3708  reu2  3718  reu2eqd  3729  sbcralt  3862  sbcreu  3866  cbvrabcsfw  3933  cbvreucsf  3936  cbvrabcsf  3937  sbcel12  4404  sbceqg  4405  2nreu  4437  csbif  4581  rexreusng  4679  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  cbvmptf  5251  cbvmptfg  5252  csbopab  5551  csbopabgALT  5552  opeliunxp  5739  ralxpf  5843  cbviotaw  6501  cbviota  6504  csbiota  6535  isarep1  6636  isarep1OLD  6637  f1ossf1o  7131  cbvriotaw  7379  cbvriota  7384  csbriota  7386  onminex  7799  tfis  7853  findes  7902  abrexex2g  7962  dfoprab4f  8054  axrepndlem1  10607  axrepndlem2  10608  uzind4s  12914  mo5f  32273  ac6sf2  32393  esumcvg  33641  bj-gabima  36354  wl-lem-moexsb  36970  wl-mo3t  36978  poimirlem26  37054  sbcalf  37522  sbcexf  37523  sbcrexgOLD  42127  scottabes  43602  2sb5nd  43922  2sb5ndALT  44294  2reu8i  46416  dfich2  46721  opeliun2xp  47319