Theorem equcomiv

Weaker form of equcomi with a disjoint variable condition on x , y. This is an intermediate step and equcomi is fully recovered later. (Contributed by BJ, 7-Dec-2020.)

Conclusion
\( \vdash x' = y' \rightarrow y' = x' \)
Proof
l0
equid
\( \vdash x' = x' \)
ax7v2
\( \vdash x' = y' \rightarrow x' = x' \rightarrow y' = x' \)
mpi l0 _