Theorem dfsb 2075

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074

This theorem is referenced by:  stdpc4  2079  sbi1  2082  spsbe  2093  sbequ  2094  sb6  2096  sbal  2180  sbequ1  2260  sbequ2  2261  dfsb7  2290  sbn  2291  sbrim  2315  cbvsbvf  2371  sb4b  2483  sbequbidv  36449  cbvsbdavw  36489  cbvsbdavw2  36490  bj-ssbeq  37000  bj-ssbid2ALT  37010  bj-ssbid1ALT  37012