Theorem nfs1v 2154

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

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1786  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069

This theorem is referenced by:  hbs1  2266  sb5OLD  2269  sb8fOLD  2351  sb8ef  2352  sbbib  2358  sb2ae  2496  mo3  2559  eu1  2607  2mo  2645  2eu6  2653  nfsab1  2718  cbvralsvw  3315  cbvrexsvw  3316  cbvralsvwOLD  3317  cbvrexsvwOLD  3318  cbvralfwOLD  3321  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvrabw  3468  cbvrab  3474  sbhypfOLD  3540  mob2  3711  reu2  3721  reu2eqd  3732  sbcralt  3866  sbcreu  3870  cbvrabcsfw  3937  cbvreucsf  3940  cbvrabcsf  3941  sbcel12  4408  sbceqg  4409  2nreu  4441  csbif  4585  rexreusng  4683  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvmptf  5257  cbvmptfg  5258  csbopab  5555  csbopabgALT  5556  opeliunxp  5742  ralxpf  5845  cbviotaw  6500  cbviota  6503  csbiota  6534  isarep1  6635  isarep1OLD  6636  f1ossf1o  7123  cbvriotaw  7371  cbvriota  7376  csbriota  7378  onminex  7787  tfis  7841  findes  7890  abrexex2g  7948  dfoprab4f  8039  axrepndlem1  10584  axrepndlem2  10585  uzind4s  12889  mo5f  31717  ac6sf2  31837  esumcvg  33073  bj-gabima  35809  wl-lem-moexsb  36422  wl-mo3t  36430  poimirlem26  36503  sbcalf  36971  sbcexf  36972  sbcrexgOLD  41509  scottabes  42987  2sb5nd  43307  2sb5ndALT  43679  2reu8i  45808  dfich2  46113  opeliun2xp  46962