Theorem nfs1v 2151

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

Syntax hints:   → wi 4  ∀wal 1537  Ⅎwnf 1783  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-10 2135

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-nf 1784  df-sb 2066

This theorem is referenced by:  hbs1  2263  sb5OLD  2266  sb8fOLD  2348  sb8ef  2349  sbbib  2355  sb2ae  2493  mo3  2556  eu1  2604  2mo  2642  2eu6  2650  nfsab1  2715  cbvralsvw  3312  cbvrexsvw  3313  cbvralsvwOLD  3314  cbvrexsvwOLD  3315  cbvralfwOLD  3318  cbvralf  3354  cbvralsv  3360  cbvrexsv  3361  cbvrabw  3465  cbvrab  3471  sbhypfOLD  3538  mob2  3712  reu2  3722  reu2eqd  3733  sbcralt  3867  sbcreu  3871  cbvrabcsfw  3938  cbvreucsf  3941  cbvrabcsf  3942  sbcel12  4409  sbceqg  4410  2nreu  4442  csbif  4586  rexreusng  4684  cbvopab1  5224  cbvopab1g  5225  cbvopab1s  5227  cbvmptf  5258  cbvmptfg  5259  csbopab  5556  csbopabgALT  5557  opeliunxp  5744  ralxpf  5847  cbviotaw  6503  cbviota  6506  csbiota  6537  isarep1  6638  isarep1OLD  6639  f1ossf1o  7129  cbvriotaw  7378  cbvriota  7383  csbriota  7385  onminex  7794  tfis  7848  findes  7897  abrexex2g  7955  dfoprab4f  8046  axrepndlem1  10591  axrepndlem2  10592  uzind4s  12898  mo5f  31994  ac6sf2  32114  esumcvg  33380  bj-gabima  36125  wl-lem-moexsb  36738  wl-mo3t  36746  poimirlem26  36819  sbcalf  37287  sbcexf  37288  sbcrexgOLD  41827  scottabes  43305  2sb5nd  43625  2sb5ndALT  43997  2reu8i  46121  dfich2  46426  opeliun2xp  47098