Theorem ax8

Proof of [ax-8] from ax8v1 and ax8v2, proving sufficiency of the conjunction of the latter two weakened versions of ax8v, which is itself a weakened version of [ax-8]. (Contributed by BJ, 7-Dec-2020.) (Proof shortened by Wolf Lammen, 11-Apr-2021.)

Conclusion
\( \vdash x' = y' \rightarrow x' \in z' \rightarrow y' \in z' \)
Proof
l0
equvinv
\( \vdash x' = y' \leftrightarrow \exists t \, (t = x' \wedge t = y') \)
ax8v2
l2
equcoms _
\( \vdash t = x' \rightarrow x' \in z' \rightarrow t \in z' \)
ax8v1
\( \vdash t = y' \rightarrow t \in z' \rightarrow y' \in z' \)
sylan9 l2 _
exlimiv _
\( \vdash \exists t \, (t = x' \wedge t = y') \rightarrow x' \in z' \rightarrow y' \in z' \)
sylbi l0 _