Theorem nfs1v 2191

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1813  [wsb 2096

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-sb 2097

This theorem is used by:  hbs1  2309  sb8ef  2387  sbbib  2393  sb2ae  2528  mo3  2592  eu1  2638  2mo  2676  2eu6  2684  nfsab1  2749  cbvrexsvw  3317  cbvralsvwOLD  3318  cbvralf  3349  cbvralsv  3355  cbvrexsv  3356  cbvrab  3454  mob2  3678  reu2  3688  reu2eqd  3699  sbcralt  3825  sbcreu  3829  cbvrabcsfw  3894  cbvreucsf  3897  cbvrabcsf  3898  sbcel12  4376  sbceqg  4377  2nreu  4409  csbif  4545  rexreusng  4645  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvmptf  5211  cbvmptfg  5212  csbopab  5540  csbopabw  5541  opeliunxp  5728  opeliun2xp  5729  ralxpf  5832  cbviotaw  6499  cbviota  6501  csbiota  6529  isarep1  6624  f1ossf1o  7124  cbvriotaw  7376  cbvriota  7380  csbriota  7382  onminex  7797  tfis  7847  findes  7893  abrexex2g  7957  dfoprab4f  8049  scottabes  9866  axrepndlem1  10581  axrepndlem2  10582  uzind4s  12936  mo5f  32844  ac6sf2  32976  esumcvg  34485  bj-gabima  37604  wl-lem-moexsb  38251  wl-mo3t  38259  poimirlem26  38325  sbcalf  38791  sbcexf  38792  2sb5nd  45297  2sb5ndALT  45668  2reu8i  47878  dfich2  48235