Theorem nfs1v 2156

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

Syntax hints:   → wi 4  ∀wal 1531  Ⅎwnf 1780  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-10 2141

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-nf 1781  df-sb 2066

This theorem is referenced by:  hbs1  2270  sb5  2272  sbbibOLD  2285  sb8v  2369  sb8ev  2370  sbbib  2376  sb2ae  2532  mo3  2644  eu1  2690  2mo  2729  2eu6  2740  nfsab1  2808  cbvralfw  3437  cbvralf  3439  cbvralsvw  3467  cbvrexsvw  3468  cbvralsv  3469  cbvrexsv  3470  cbvrabw  3489  cbvrab  3490  sbhypf  3552  mob2  3705  reu2  3715  reu2eqd  3726  sbcralt  3854  sbcreu  3858  cbvrabcsfw  3923  cbvreucsf  3926  cbvrabcsf  3927  sbcel12  4359  sbceqg  4360  2nreu  4392  csbif  4521  rexreusng  4610  cbvopab1  5131  cbvopab1g  5132  cbvopab1s  5134  cbvmptf  5157  cbvmptfg  5158  opelopabsb  5409  csbopab  5434  csbopabgALT  5435  opeliunxp  5613  ralxpf  5711  cbviotaw  6315  cbviota  6317  csbiota  6342  isarep1  6436  f1ossf1o  6884  cbvriotaw  7117  cbvriota  7121  csbriota  7123  onminex  7516  tfis  7563  findes  7606  abrexex2g  7659  dfoprab4f  7748  axrepndlem1  10008  axrepndlem2  10009  uzind4s  12302  mo5f  30247  ac6sf2  30364  esumcvg  31340  wl-lem-moexsb  34798  wl-mo3t  34806  poimirlem26  34912  sbcalf  35386  sbcexf  35387  sbcrexgOLD  39375  scottabes  40571  2sb5nd  40887  2sb5ndALT  41259  2reu8i  43306  dfich2  43607  dfich2ai  43608  dfich2OLD  43610  ichnfimlem2  43616  opeliun2xp  44375