Description: An equivalence of substitutions (as in sbbii ) allowing the additional information that x = t . Version of sbiev and sbievw without a disjoint variable condition on ps , useful for substituting only part of ph . (Contributed by SN, 24-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbbiiev.1 | |- ( x = t -> ( ph <-> ps ) ) |
|
| Assertion | sbbiiev | |- ( [ t / x ] ph <-> [ t / x ] ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbbiiev.1 | |- ( x = t -> ( ph <-> ps ) ) |
|
| 2 | 1 | pm5.74i | |- ( ( x = t -> ph ) <-> ( x = t -> ps ) ) |
| 3 | 2 | albii | |- ( A. x ( x = t -> ph ) <-> A. x ( x = t -> ps ) ) |
| 4 | sb6 | |- ( [ t / x ] ph <-> A. x ( x = t -> ph ) ) |
|
| 5 | sb6 | |- ( [ t / x ] ps <-> A. x ( x = t -> ps ) ) |
|
| 6 | 3 4 5 | 3bitr4i | |- ( [ t / x ] ph <-> [ t / x ] ps ) |