Theorem nfs1v 2191

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

Syntax hints:   → wi 4  ∀wal 1559  Ⅎwnf 1804  [wsb 2091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-10 2176

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1801  df-nf 1805  df-sb 2092

This theorem is referenced by:  hbs1  2309  sb8ef  2387  sbbib  2393  sb2ae  2528  mo3  2592  eu1  2638  2mo  2676  2eu6  2684  nfsab1  2749  cbvrexsvw  3315  cbvralsvwOLD  3316  cbvralf  3348  cbvralsv  3354  cbvrexsv  3355  cbvrabwOLD  3451  cbvrab  3454  mob2  3679  reu2  3689  reu2eqd  3700  sbcralt  3826  sbcreu  3830  cbvrabcsfw  3894  cbvreucsf  3897  cbvrabcsf  3898  sbcel12  4366  sbceqg  4367  2nreu  4399  csbif  4539  rexreusng  4639  cbvopab1  5175  cbvopab1g  5176  cbvopab1s  5178  cbvmptf  5201  cbvmptfg  5202  csbopab  5527  csbopabw  5528  opeliunxp  5715  opeliun2xp  5716  ralxpf  5819  cbviotaw  6485  cbviota  6487  csbiota  6515  isarep1  6611  f1ossf1o  7111  cbvriotaw  7363  cbvriota  7367  csbriota  7369  onminex  7786  tfis  7836  findes  7882  abrexex2g  7946  dfoprab4f  8038  axrepndlem1  10551  axrepndlem2  10552  uzind4s  12910  mo5f  32689  ac6sf2  32825  esumcvg  34384  bj-gabima  37426  wl-lem-moexsb  38072  wl-mo3t  38080  poimirlem26  38146  sbcalf  38614  sbcexf  38615  scottabes  44819  2sb5nd  45137  2sb5ndALT  45508  2reu8i  47708  dfich2  48065