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  2207  sbequ1  2287  sbequ2  2288  dfsb7  2317  sbn  2318  sbrim  2342  cbvsbvf  2398  sb4b  2510  sbequbidv  36767  cbvsbdavw  36807  cbvsbdavw2  36808  bj-ssbeq  37316  bj-ssbid2ALT  37326  bj-ssbid1ALT  37328