Metamath Proof Explorer


Theorem sbeqi

Description: Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Assertion sbeqi ( ( 𝑥 = 𝑦 ∧ ∀ 𝑧 ( 𝜑𝜓 ) ) → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑧 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 spsbbi ( ∀ 𝑧 ( 𝜑𝜓 ) → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑥 / 𝑧 ] 𝜓 ) )
2 sbequ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑧 ] 𝜓 ) )
3 1 2 sylan9bbr ( ( 𝑥 = 𝑦 ∧ ∀ 𝑧 ( 𝜑𝜓 ) ) → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑧 ] 𝜓 ) )