Theorem nfs1v 2162

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1785  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069

This theorem is referenced by:  hbs1  2281  sb8ef  2360  sbbib  2366  sb2ae  2501  mo3  2565  eu1  2611  2mo  2649  2eu6  2658  nfsab1  2723  cbvrexsvw  3290  cbvralsvwOLD  3291  cbvralsvwOLDOLD  3292  cbvrexsvwOLD  3293  cbvralf  3332  cbvralsv  3338  cbvrexsv  3339  cbvrabwOLD  3437  cbvrab  3441  mob2  3675  reu2  3685  reu2eqd  3696  sbcralt  3824  sbcreu  3828  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4365  sbceqg  4366  2nreu  4398  csbif  4539  rexreusng  4638  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  cbvmptf  5200  cbvmptfg  5201  csbopab  5511  csbopabgALT  5512  opeliunxp  5699  opeliun2xp  5700  ralxpf  5803  cbviotaw  6463  cbviota  6465  csbiota  6493  isarep1  6589  f1ossf1o  7083  cbvriotaw  7334  cbvriota  7338  csbriota  7340  onminex  7757  tfis  7807  findes  7852  abrexex2g  7918  dfoprab4f  8010  axrepndlem1  10515  axrepndlem2  10516  uzind4s  12833  mo5f  32579  ac6sf2  32716  esumcvg  34268  bj-gabima  37192  wl-lem-moexsb  37827  wl-mo3t  37835  poimirlem26  37901  sbcalf  38369  sbcexf  38370  sbcrexgOLD  43146  scottabes  44602  2sb5nd  44920  2sb5ndALT  45291  2reu8i  47477  dfich2  47822