Theorem nfs1v 2159

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

Syntax hints:   → wi 4  ∀wal 1539  Ⅎwnf 1784  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068

This theorem is referenced by:  hbs1  2276  sb8ef  2355  sbbib  2361  sb2ae  2496  mo3  2559  eu1  2605  2mo  2643  2eu6  2652  nfsab1  2717  cbvrexsvw  3284  cbvralsvwOLD  3285  cbvralsvwOLDOLD  3286  cbvrexsvwOLD  3287  cbvralf  3326  cbvralsv  3332  cbvrexsv  3333  cbvrabwOLD  3431  cbvrab  3435  mob2  3669  reu2  3679  reu2eqd  3690  sbcralt  3818  sbcreu  3822  cbvrabcsfw  3886  cbvreucsf  3889  cbvrabcsf  3890  sbcel12  4358  sbceqg  4359  2nreu  4391  csbif  4530  rexreusng  4629  cbvopab1  5163  cbvopab1g  5164  cbvopab1s  5166  cbvmptf  5189  cbvmptfg  5190  csbopab  5493  csbopabgALT  5494  opeliunxp  5681  opeliun2xp  5682  ralxpf  5785  cbviotaw  6444  cbviota  6446  csbiota  6474  isarep1  6570  f1ossf1o  7061  cbvriotaw  7312  cbvriota  7316  csbriota  7318  onminex  7735  tfis  7785  findes  7830  abrexex2g  7896  dfoprab4f  7988  axrepndlem1  10483  axrepndlem2  10484  uzind4s  12806  mo5f  32468  ac6sf2  32605  esumcvg  34099  bj-gabima  36984  wl-lem-moexsb  37612  wl-mo3t  37620  poimirlem26  37696  sbcalf  38164  sbcexf  38165  sbcrexgOLD  42888  scottabes  44345  2sb5nd  44663  2sb5ndALT  45034  2reu8i  47223  dfich2  47568