Theorem nfs1v 2154

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069

This theorem is referenced by:  hbs1  2266  sb5OLD  2269  sb8fOLD  2351  sb8ef  2352  sbbib  2358  sb2ae  2496  mo3  2559  eu1  2607  2mo  2645  2eu6  2653  nfsab1  2718  cbvralsvw  3315  cbvrexsvw  3316  cbvralsvwOLD  3317  cbvrexsvwOLD  3318  cbvralfwOLD  3321  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvrabw  3468  cbvrab  3474  sbhypfOLD  3540  mob2  3712  reu2  3722  reu2eqd  3733  sbcralt  3867  sbcreu  3871  cbvrabcsfw  3938  cbvreucsf  3941  cbvrabcsf  3942  sbcel12  4409  sbceqg  4410  2nreu  4442  csbif  4586  rexreusng  4684  cbvopab1  5224  cbvopab1g  5225  cbvopab1s  5227  cbvmptf  5258  cbvmptfg  5259  csbopab  5556  csbopabgALT  5557  opeliunxp  5744  ralxpf  5847  cbviotaw  6503  cbviota  6506  csbiota  6537  isarep1  6638  isarep1OLD  6639  f1ossf1o  7126  cbvriotaw  7374  cbvriota  7379  csbriota  7381  onminex  7790  tfis  7844  findes  7893  abrexex2g  7951  dfoprab4f  8042  axrepndlem1  10587  axrepndlem2  10588  uzind4s  12892  mo5f  31729  ac6sf2  31849  esumcvg  33084  bj-gabima  35820  wl-lem-moexsb  36433  wl-mo3t  36441  poimirlem26  36514  sbcalf  36982  sbcexf  36983  sbcrexgOLD  41523  scottabes  43001  2sb5nd  43321  2sb5ndALT  43693  2reu8i  45821  dfich2  46126  opeliun2xp  47008