Theorem dfsb 2069

Description: Simplify definition df-sb 2068 by removing its provable hypothesis. (Contributed by Wolf Lammen, 5-Feb-2026.)

Assertion

Ref	Expression
dfsb	⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Distinct variable groups:   𝑥,𝑦   𝑦,𝑡   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑡)

Proof of Theorem dfsb

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbjust 2066	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
2	1	df-sb 2068	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  [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

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

This theorem is referenced by:  stdpc4  2073  sbi1  2076  spsbe  2087  sbequ  2088  sb6  2090  sbal  2174  hbsbwOLD  2177  sbequ1  2253  sbequ2  2254  dfsb7  2283  sbn  2284  sbrim  2308  cbvsbvf  2365  sb4b  2477  sbequbidv  36269  cbvsbdavw  36309  cbvsbdavw2  36310  bj-ssbeq  36708  bj-ssbid2ALT  36718  bj-ssbid1ALT  36720