Description: Version of hbsb2 with a disjoint variable condition, which does not require ax-13 , and removal of ax-13 from hbs1 . (Contributed by BJ, 23-Jun-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-hbs1 | |- ( [ y / x ] ph -> A. x [ y / x ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb6 | |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) |
|
| 2 | 1 | biimpri | |- ( A. x ( x = y -> ph ) -> [ y / x ] ph ) |
| 3 | 2 | axc4i | |- ( A. x ( x = y -> ph ) -> A. x [ y / x ] ph ) |
| 4 | 1 3 | sylbi | |- ( [ y / x ] ph -> A. x [ y / x ] ph ) |