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

Syntax hints:   → wi 4  ∀wal 1536  Ⅎwnf 1785  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070

This theorem is referenced by:  hbs1  2271  sb5  2273  sbbibOLD  2285  sb8v  2362  sb8ev  2363  sbbib  2369  sb2ae  2514  mo3  2623  eu1  2671  2mo  2710  2eu6  2719  nfsab1  2785  cbvralfwOLD  3383  cbvralf  3385  cbvralsvw  3414  cbvrexsvw  3415  cbvralsv  3416  cbvrexsv  3417  cbvrabw  3437  cbvrab  3438  sbhypf  3500  mob2  3654  reu2  3664  reu2eqd  3675  sbcralt  3801  sbcreu  3805  cbvrabcsfw  3869  cbvreucsf  3872  cbvrabcsf  3873  sbcel12  4316  sbceqg  4317  2nreu  4349  csbif  4480  rexreusng  4577  cbvopab1  5103  cbvopab1g  5104  cbvopab1s  5106  cbvmptf  5129  cbvmptfg  5130  opelopabsb  5382  csbopab  5407  csbopabgALT  5408  opeliunxp  5583  ralxpf  5681  cbviotaw  6290  cbviota  6292  csbiota  6317  isarep1  6412  f1ossf1o  6867  cbvriotaw  7102  cbvriota  7106  csbriota  7108  onminex  7502  tfis  7549  findes  7593  abrexex2g  7647  dfoprab4f  7736  axrepndlem1  10003  axrepndlem2  10004  uzind4s  12296  mo5f  30260  ac6sf2  30384  esumcvg  31455  wl-lem-moexsb  34969  wl-mo3t  34977  poimirlem26  35083  sbcalf  35552  sbcexf  35553  sbcrexgOLD  39726  scottabes  40950  2sb5nd  41266  2sb5ndALT  41638  2reu8i  43669  dfich2  43975  opeliun2xp  44734