Theorem nfs1v 2161

Description: The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2161 and hbs1 2278 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 2156	. 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 2146

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  2278  sb8ef  2357  sbbib  2363  sb2ae  2498  mo3  2562  eu1  2608  2mo  2646  2eu6  2655  nfsab1  2720  cbvrexsvw  3286  cbvralsvwOLD  3287  cbvralsvwOLDOLD  3288  cbvrexsvwOLD  3289  cbvralf  3328  cbvralsv  3334  cbvrexsv  3335  cbvrabwOLD  3433  cbvrab  3437  mob2  3671  reu2  3681  reu2eqd  3692  sbcralt  3820  sbcreu  3824  cbvrabcsfw  3888  cbvreucsf  3891  cbvrabcsf  3892  sbcel12  4361  sbceqg  4362  2nreu  4394  csbif  4535  rexreusng  4634  cbvopab1  5170  cbvopab1g  5171  cbvopab1s  5173  cbvmptf  5196  cbvmptfg  5197  csbopab  5501  csbopabgALT  5502  opeliunxp  5689  opeliun2xp  5690  ralxpf  5793  cbviotaw  6453  cbviota  6455  csbiota  6483  isarep1  6579  f1ossf1o  7071  cbvriotaw  7322  cbvriota  7326  csbriota  7328  onminex  7745  tfis  7795  findes  7840  abrexex2g  7906  dfoprab4f  7998  axrepndlem1  10501  axrepndlem2  10502  uzind4s  12819  mo5f  32512  ac6sf2  32649  esumcvg  34192  bj-gabima  37084  wl-lem-moexsb  37712  wl-mo3t  37720  poimirlem26  37786  sbcalf  38254  sbcexf  38255  sbcrexgOLD  42969  scottabes  44425  2sb5nd  44743  2sb5ndALT  45114  2reu8i  47301  dfich2  47646