Theorem dfsb 2101

Description: Simplify definition df-sb 2100 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 2098	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
2	1	df-sb 2100	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  stdpc4  2105  sbi1  2108  spsbe  2119  sbequ  2120  sb6  2122  sbal  2206  sbequ1  2284  sbequ2  2285  dfsb7  2313  sbn  2314  sbrim  2338  cbvsbvf  2393  sb4b  2505  sbequbidv  36973  cbvsbdavw  37013  cbvsbdavw2  37014  bj-ssbeq  37522  bj-ssbid2ALT  37532  bj-ssbid1ALT  37534