Theorem bj-df-sb 36769

Description: Proposed definition to replace df-sb 2068 and df-sbc 3738. Proof is therefore unimportant. Contrary to df-sb 2068, this definition makes a substituted formula false when one substitutes a non-existent object for a variable: this is better suited to the "Levy-style" treatment of classes as virtual objects adopted by set.mm. The equality 𝑦 = 𝑥 may seem "reversed", but it is written this way so that "substitution for oneself" does not require symmetry of equality to be seen to be the identity on propositions. (Contributed by BJ, 19-Feb-2026.)

Assertion

Ref	Expression
bj-df-sb	⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑦 = 𝑥 → 𝜑)))

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

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem bj-df-sb

Step	Hyp	Ref	Expression
1		sbc7 3769	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑))
2		sb6 2090	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
3		sbsbc 3741	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
4		equcom 2019	. . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
5	4	imbi1i 349	. . . . . 6 ⊢ ((𝑥 = 𝑦 → 𝜑) ↔ (𝑦 = 𝑥 → 𝜑))
6	5	albii 1820	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑))
7	2, 3, 6	3bitr3i 301	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑))
8	7	anbi2i 623	. . 3 ⊢ ((𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝑦 = 𝐴 ∧ ∀𝑥(𝑦 = 𝑥 → 𝜑)))
9	8	exbii 1849	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑦 = 𝑥 → 𝜑)))
10	1, 9	bitri 275	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑦 = 𝑥 → 𝜑)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780  [wsb 2067  [wsbc 3737

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  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-sbc 3738

This theorem is referenced by: (None)