Theorem ax9

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

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