Theorem nfs1v 2145

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

Syntax hints:   → wi 4  ∀wal 1531  Ⅎwnf 1777  [wsb 2059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-sb 2060

This theorem is referenced by:  hbs1  2260  sb5OLD  2263  sb8fOLD  2344  sb8ef  2345  sbbib  2351  sb2ae  2489  mo3  2552  eu1  2598  2mo  2636  2eu6  2645  nfsab1  2710  cbvralsvw  3305  cbvrexsvw  3306  cbvralsvwOLD  3307  cbvrexsvwOLD  3308  cbvralf  3344  cbvralsv  3350  cbvrexsv  3351  cbvrabw  3456  cbvrab  3462  sbhypfOLD  3530  mob2  3708  reu2  3718  reu2eqd  3729  sbcralt  3863  sbcreu  3867  cbvrabcsfw  3934  cbvreucsf  3937  cbvrabcsf  3938  sbcel12  4409  sbceqg  4410  2nreu  4442  csbif  4586  rexreusng  4684  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvmptf  5257  cbvmptfg  5258  csbopab  5556  csbopabgALT  5557  opeliunxp  5744  ralxpf  5848  cbviotaw  6506  cbviota  6509  csbiota  6540  isarep1  6641  isarep1OLD  6642  f1ossf1o  7135  cbvriotaw  7382  cbvriota  7387  csbriota  7389  onminex  7804  tfis  7858  findes  7906  abrexex2g  7967  dfoprab4f  8059  axrepndlem1  10615  axrepndlem2  10616  uzind4s  12922  mo5f  32344  ac6sf2  32467  esumcvg  33775  bj-gabima  36488  wl-lem-moexsb  37105  wl-mo3t  37113  poimirlem26  37189  sbcalf  37657  sbcexf  37658  sbcrexgOLD  42270  scottabes  43744  2sb5nd  44064  2sb5ndALT  44436  2reu8i  46556  dfich2  46861  opeliun2xp  47508