Theorem equvel
A variable elimination law for equality with no distinct variable
requirements. Compare equvini. Usage of this theorem is discouraged
because it depends on [ax-13]. Use equvelv when possible.
(Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro,
17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.)
(New usage is discouraged.)
Conclusion
\( \vdash \forall z \, (z = x' \leftrightarrow z = y') \rightarrow x' = y' \)
Proof
l0
albi
\( \vdash \forall z \, (z = x' \leftrightarrow z = y') \rightarrow (\forall z \, z = x' \leftrightarrow \forall z \, z = y') \)
l1
ax6e
\( \vdash \exists z \, z = y' \)
l2
biimpr
\( \vdash (z = x' \leftrightarrow z = y') \rightarrow z = y' \rightarrow z = x' \)
l3
ax7
\( \vdash z = x' \rightarrow z = y' \rightarrow x' = y' \)
syli l2 _
com12 _
\( \vdash z = y' \rightarrow (z = x' \leftrightarrow z = y') \rightarrow x' = y' \)
eximii l1 _
l7
19.35i _
\( \vdash \forall z \, (z = x' \leftrightarrow z = y') \rightarrow \exists z \, x' = y' \)
spsd l3
sps _
l10
a1dd _
nfeqf
19.9d _
ex _
bija l10 _
\( \vdash (\forall z \, z = x' \leftrightarrow \forall z \, z = y') \rightarrow \exists z \, x' = y' \rightarrow x' = y' \)
sylc l0 l7 _