Theorem aeveq

The antecedent \( \forall x \, x = y' \) with a disjoint variable condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow z' = t' \)
Proof
l0
cbvaev
\( \vdash \forall x \, x = y' \rightarrow \forall w \, w = y' \)
l1
ax6ev
\( \vdash \exists w \, w = z' \)
l2
ax7
l3
aleximi _
l4
mpi l1 _
l5
ax5e
l6
3syl l0 l4 _
\( \vdash \forall x \, x = y' \rightarrow y' = z' \)
l7
ax6ev
\( \vdash \exists w \, w = t' \)
l8
ax7
l9
aleximi _
l10
mpi l7 _
l11
ax5e
l12
3syl l0 l10 _
\( \vdash \forall x \, x = y' \rightarrow y' = t' \)
l13
ax7
l14
sylc l6 l12 _