Theorem nfs1v 2157

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  hbs1  2274  sb8fOLD  2353  sb8ef  2354  sbbib  2360  sb2ae  2495  mo3  2558  eu1  2604  2mo  2642  2eu6  2651  nfsab1  2716  cbvrexsvw  3293  cbvralsvwOLD  3294  cbvralsvwOLDOLD  3295  cbvrexsvwOLD  3296  cbvralf  3336  cbvralsv  3342  cbvrexsv  3343  cbvrabwOLD  3445  cbvrab  3449  sbhypfOLD  3514  mob2  3688  reu2  3698  reu2eqd  3709  sbcralt  3837  sbcreu  3841  cbvrabcsfw  3905  cbvreucsf  3908  cbvrabcsf  3909  sbcel12  4376  sbceqg  4377  2nreu  4409  csbif  4548  rexreusng  4645  cbvopab1  5183  cbvopab1g  5184  cbvopab1s  5186  cbvmptf  5209  cbvmptfg  5210  csbopab  5517  csbopabgALT  5518  opeliunxp  5707  opeliun2xp  5708  ralxpf  5812  cbviotaw  6473  cbviota  6475  csbiota  6506  isarep1  6608  isarep1OLD  6609  f1ossf1o  7102  cbvriotaw  7355  cbvriota  7359  csbriota  7361  onminex  7780  tfis  7833  findes  7878  abrexex2g  7945  dfoprab4f  8037  axrepndlem1  10551  axrepndlem2  10552  uzind4s  12873  mo5f  32424  ac6sf2  32554  esumcvg  34082  bj-gabima  36923  wl-lem-moexsb  37551  wl-mo3t  37559  poimirlem26  37635  sbcalf  38103  sbcexf  38104  sbcrexgOLD  42766  scottabes  44224  2sb5nd  44543  2sb5ndALT  44914  2reu8i  47104  dfich2  47449