Theorem sbeqi

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

	Ref	Expression
Assertion	sbeqi	$$⊢\left(x=y\wedge \forall z\left(\phi \leftrightarrow \psi \right)\right)\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spsbbi	$$⊢\forall z\left(\phi \leftrightarrow \psi \right)\to \left(\left[x/z\right]\phi \leftrightarrow \left[x/z\right]\psi \right)$$
2		sbequ	$$⊢x=y\to \left(\left[x/z\right]\psi \leftrightarrow \left[y/z\right]\psi \right)$$
3	1 2	sylan9bbr	$$⊢\left(x=y\wedge \forall z\left(\phi \leftrightarrow \psi \right)\right)\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\psi \right)$$