Theorem ax7

Proof of [ax-7] from ax7v1 and ax7v2 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v, which is itself a weakened version of [ax-7].

Note that the weakened version of [ax-7] obtained by adding a disjoint variable condition on x , z (resp. on y , z) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.)

Conclusion
\( \vdash x' = y' \rightarrow x' = z' \rightarrow y' = z' \)
Proof
l0
ax7v2
\( \vdash x' = t \rightarrow x' = y' \rightarrow t = y' \)
l1
ax7v2
\( \vdash x' = t \rightarrow x' = z' \rightarrow t = z' \)
ax7v1
imp _
a1i _
\( \vdash x' = t \rightarrow t = y' \wedge t = z' \rightarrow y' = z' \)
l5
syl2and l0 l1 _
\( \vdash x' = t \rightarrow x' = y' \wedge x' = z' \rightarrow y' = z' \)
ax6evr
\( \vdash \exists t \, x' = t \)
exlimiiv l5 _
ex _