Description: One direction of sb5 , provable from fewer axioms. Version of sb1 with a disjoint variable condition using fewer axioms. (Contributed by NM, 13-May-1993) (Revised by Wolf Lammen, 20-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sb1v | |- ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb6 | |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) |
|
| 2 | equs4v | |- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) ) |
|
| 3 | 1 2 | sylbi | |- ( [ y / x ] ph -> E. x ( x = y /\ ph ) ) |