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 | ⊢ ( 𝑥 = 𝑡 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | sbbiiev | ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ [ 𝑡 / 𝑥 ] 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbbiiev.1 | ⊢ ( 𝑥 = 𝑡 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | 1 | pm5.74i | ⊢ ( ( 𝑥 = 𝑡 → 𝜑 ) ↔ ( 𝑥 = 𝑡 → 𝜓 ) ) |
| 3 | 2 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) |
| 4 | sb6 | ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜑 ) ) | |
| 5 | sb6 | ⊢ ( [ 𝑡 / 𝑥 ] 𝜓 ↔ ∀ 𝑥 ( 𝑥 = 𝑡 → 𝜓 ) ) | |
| 6 | 3 4 5 | 3bitr4i | ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ [ 𝑡 / 𝑥 ] 𝜓 ) |