Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim and sbrimv based on fewer axioms, but with more disjoint variable conditions. Based on an idea of Gino Giotto. (Contributed by Wolf Lammen, 29-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbrimvw | |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.21v | |- ( A. x ( ph -> ( x = y -> ps ) ) <-> ( ph -> A. x ( x = y -> ps ) ) ) |
|
| 2 | 1 | sbrimvlem | |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) |