Theorem equsb3r

Description: Substitution applied to the atomic wff with equality. Variant of equsb3 . (Contributed by AV, 29-Jul-2023) (Proof shortened by Wolf Lammen, 2-Sep-2023)

	Ref	Expression
Assertion	equsb3r	$$⊢\left[y/x\right]z=x\leftrightarrow z=y$$

Proof

Step	Hyp	Ref	Expression
1		equequ2	$$⊢x=w\to \left(z=x\leftrightarrow z=w\right)$$
2		equequ2	$$⊢w=y\to \left(z=w\leftrightarrow z=y\right)$$
3	1 2	sbievw2	$$⊢\left[y/x\right]z=x\leftrightarrow z=y$$