Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw ). Version of sbied and sbiedv with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994) (Revised by Gino Giotto, 29-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbiedvw.1 | |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) |
|
| Assertion | sbiedvw | |- ( ph -> ( [ y / x ] ps <-> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbiedvw.1 | |- ( ( ph /\ x = y ) -> ( ps <-> ch ) ) |
|
| 2 | sbrimvw | |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) |
|
| 3 | 1 | expcom | |- ( x = y -> ( ph -> ( ps <-> ch ) ) ) |
| 4 | 3 | pm5.74d | |- ( x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) ) |
| 5 | 4 | sbievw | |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> ch ) ) |
| 6 | 2 5 | bitr3i | |- ( ( ph -> [ y / x ] ps ) <-> ( ph -> ch ) ) |
| 7 | 6 | pm5.74ri | |- ( ph -> ( [ y / x ] ps <-> ch ) ) |