Description: Proposed definition to replace df-sb and df-sbc . Proof is therefore unimportant. Contrary to df-sb , 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 y = x 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-df-sb | |- ( [. A / x ]. ph <-> E. y ( y = A /\ A. x ( y = x -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbc7 | |- ( [. A / x ]. ph <-> E. y ( y = A /\ [. y / x ]. ph ) ) |
|
| 2 | sb6 | |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) |
|
| 3 | sbsbc | |- ( [ y / x ] ph <-> [. y / x ]. ph ) |
|
| 4 | equcom | |- ( x = y <-> y = x ) |
|
| 5 | 4 | imbi1i | |- ( ( x = y -> ph ) <-> ( y = x -> ph ) ) |
| 6 | 5 | albii | |- ( A. x ( x = y -> ph ) <-> A. x ( y = x -> ph ) ) |
| 7 | 2 3 6 | 3bitr3i | |- ( [. y / x ]. ph <-> A. x ( y = x -> ph ) ) |
| 8 | 7 | anbi2i | |- ( ( y = A /\ [. y / x ]. ph ) <-> ( y = A /\ A. x ( y = x -> ph ) ) ) |
| 9 | 8 | exbii | |- ( E. y ( y = A /\ [. y / x ]. ph ) <-> E. y ( y = A /\ A. x ( y = x -> ph ) ) ) |
| 10 | 1 9 | bitri | |- ( [. A / x ]. ph <-> E. y ( y = A /\ A. x ( y = x -> ph ) ) ) |