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 2275 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 2085	. 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
2		nfa1 2152	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑦 → 𝜑)
3	1, 2	nfxfr 1851	1 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑

Syntax hints:   → wi 4  ∀wal 1535  Ⅎwnf 1781  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065

This theorem is referenced by:  hbs1  2275  sb5OLD  2278  sb8fOLD  2360  sb8ef  2361  sbbib  2367  sb2ae  2504  mo3  2567  eu1  2613  2mo  2651  2eu6  2660  nfsab1  2725  cbvrexsvw  3324  cbvralsvwOLD  3325  cbvralsvwOLDOLD  3326  cbvrexsvwOLD  3327  cbvralf  3368  cbvralsv  3374  cbvrexsv  3375  cbvrabwOLD  3482  cbvrab  3487  sbhypfOLD  3557  mob2  3737  reu2  3747  reu2eqd  3758  sbcralt  3894  sbcreu  3898  cbvrabcsfw  3965  cbvreucsf  3968  cbvrabcsf  3969  sbcel12  4434  sbceqg  4435  2nreu  4467  csbif  4605  rexreusng  4703  cbvopab1  5241  cbvopab1g  5242  cbvopab1s  5244  cbvmptf  5275  cbvmptfg  5276  csbopab  5574  csbopabgALT  5575  opeliunxp  5767  ralxpf  5871  cbviotaw  6534  cbviota  6537  csbiota  6568  isarep1  6669  isarep1OLD  6670  f1ossf1o  7164  cbvriotaw  7415  cbvriota  7420  csbriota  7422  onminex  7840  tfis  7894  findes  7942  abrexex2g  8007  dfoprab4f  8099  axrepndlem1  10663  axrepndlem2  10664  uzind4s  12975  mo5f  32519  ac6sf2  32646  esumcvg  34052  bj-gabima  36908  wl-lem-moexsb  37524  wl-mo3t  37532  poimirlem26  37608  sbcalf  38076  sbcexf  38077  sbcrexgOLD  42743  scottabes  44213  2sb5nd  44533  2sb5ndALT  44905  2reu8i  47030  dfich2  47334  opeliun2xp  48059