Description: Conversion of implicit substitution to explicit substitution (deduction version of sbiev ). Version of sbied with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994) (Revised by Gino Giotto, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 28-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | sbiedw.1 | |- F/ x ph |
|
| sbiedw.2 | |- ( ph -> F/ x ch ) |
||
| sbiedw.3 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
||
| Assertion | sbiedw | |- ( ph -> ( [ y / x ] ps <-> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbiedw.1 | |- F/ x ph |
|
| 2 | sbiedw.2 | |- ( ph -> F/ x ch ) |
|
| 3 | sbiedw.3 | |- ( ph -> ( x = y -> ( ps <-> ch ) ) ) |
|
| 4 | 1 | sbrimv | |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) |
| 5 | 1 2 | nfim1 | |- F/ x ( ph -> ch ) |
| 6 | 3 | com12 | |- ( x = y -> ( ph -> ( ps <-> ch ) ) ) |
| 7 | 6 | pm5.74d | |- ( x = y -> ( ( ph -> ps ) <-> ( ph -> ch ) ) ) |
| 8 | 5 7 | sbiev | |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> ch ) ) |
| 9 | 4 8 | bitr3i | |- ( ( ph -> [ y / x ] ps ) <-> ( ph -> ch ) ) |
| 10 | 9 | pm5.74ri | |- ( ph -> ( [ y / x ] ps <-> ch ) ) |