Theorem dfsb 2092

Description: Simplify definition df-sb 2090 by proving the renaming independency. (Contributed by Wolf Lammen, 5-Feb-2026.) df-sb 2090 changed. (Revised by Wolf Lammen, 4-Jun-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		dfsbimp 2091	. 2 ⊢ ([𝑡 / 𝑥]𝜑 → ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		df-sb 2090	. . 3 ⊢ ([𝑡 / 𝑥]𝜑 ↔ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ∧ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))))
3		rename-sb 2088	. . 3 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
4	2, 3	just3-df 2087	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) → [𝑡 / 𝑥]𝜑)
5	1, 4	impbii 211	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557  [wsb 2089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090

This theorem is referenced by:  stdpc4ALT  2098  sbi1ALT  2103  sbequ  2115  sb6  2117  sbal  2202  sbequ1  2282  dfsb7  2312  sbn  2313  sbrim  2337  cbvsbvf  2393  sb4b  2505  sbequbidv  36538  cbvsbdavw  36578  cbvsbdavw2  36579  bj-ssbeq  37089  bj-ssbid2ALT  37099  bj-ssbid1ALT  37101