Theorem bj-df-sb 37642

Description: Proposed definition to replace df-sb 2099 and df-sbc 3739. Proof is therefore unimportant. Contrary to df-sb 2099, 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. Indeed, in most set theories, and in particular in this database, one wants to be able to collect the extension of a formula, so it is natural that the extension of a formula contain only sets, and not proper classes. This is illustrated by the fact that bj-dfsbc 37644 holds unconditionally. That statement could therefore replace df-clab 2739.

This definition is equivalent to df-sb 2099 when a setvar is substituted for the class, since, as soon as, ax6ev 2001 is posited, all variables "exist". (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 3770	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑))
2		sbsbc 3742	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
3		sb6 2121	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
4	2, 3	bitr3i 280	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
5	4	anbi2i 635	. . 3 ⊢ ((𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ (𝑦 = 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
6	5	exbii 1880	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
7	1, 6	bitri 278	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811  [wsb 2098  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sbc 3739

This theorem is used by:  bj-sbcex  37643  bj-dfsbc  37644