Theorem nfs1v 2197

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

Syntax hints:   → wi 4  ∀wal 1565  Ⅎwnf 1810  [wsb 2097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-sb 2098

This theorem is referenced by:  hbs1  2315  sb8ef  2393  sbbib  2399  sb2ae  2534  mo3  2598  eu1  2644  2mo  2682  2eu6  2690  nfsab1  2755  cbvrexsvw  3323  cbvralsvwOLD  3324  cbvralf  3356  cbvralsv  3362  cbvrexsv  3363  cbvrabwOLD  3459  cbvrab  3462  mob2  3687  reu2  3697  reu2eqd  3708  sbcralt  3834  sbcreu  3838  cbvrabcsfw  3902  cbvreucsf  3905  cbvrabcsf  3906  sbcel12  4382  sbceqg  4383  2nreu  4415  csbif  4550  rexreusng  4650  cbvopab1  5189  cbvopab1g  5190  cbvopab1s  5192  cbvmptf  5215  cbvmptfg  5216  csbopab  5541  csbopabw  5542  opeliunxp  5729  opeliun2xp  5730  ralxpf  5833  cbviotaw  6500  cbviota  6502  csbiota  6530  isarep1  6625  f1ossf1o  7125  cbvriotaw  7377  cbvriota  7381  csbriota  7383  onminex  7801  tfis  7851  findes  7897  abrexex2g  7961  dfoprab4f  8053  scottabes  9868  axrepndlem1  10577  axrepndlem2  10578  uzind4s  12932  mo5f  32776  ac6sf2  32908  esumcvg  34421  bj-gabima  37498  wl-lem-moexsb  38145  wl-mo3t  38153  poimirlem26  38219  sbcalf  38687  sbcexf  38688  2sb5nd  45195  2sb5ndALT  45566  2reu8i  47773  dfich2  48130