Theorem equsb3r

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.)

Conclusion
\( \vdash [ y' / x ] \, z' = x \leftrightarrow z' = y' \)
Proof
l0
equequ2
\( \vdash x = w \rightarrow (z' = x \leftrightarrow z' = w) \)
equequ2
\( \vdash w = y' \rightarrow (z' = w \leftrightarrow z' = y') \)
sbievw2 l0 _