Description: Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | sbeqi | ⊢ ( ( 𝑥 = 𝑦 ∧ ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ) → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑧 ] 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spsbbi | ⊢ ( ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] 𝜓 ) ) | |
2 | sbequ | ⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑧 ] 𝜓 ) ) | |
3 | 1 2 | sylan9bbr | ⊢ ( ( 𝑥 = 𝑦 ∧ ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ) → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑧 ] 𝜓 ) ) |