Theorem equvelv

A biconditional form of equvel with disjoint variable conditions and proved from Tarski's FOL axiom schemes. (Contributed by Andrew Salmon, 2-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)

Conclusion
\( \vdash \forall z \, (z = x' \rightarrow z = y') \leftrightarrow x' = y' \)
Proof
equequ1
equsalvw _