Theorem equvinv

A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on [ax-10], [ax-13]. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable ( \( z \)) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.)

Conclusion
\( \vdash x' = y' \leftrightarrow \exists z \, (z = x' \wedge z = y') \)
Proof
equequ1
equsexvw _
bicomi _