Theorem equvini
A variable introduction law for equality. Lemma 15 of [Monk2] p. 109,
however we do not require \( z \) to be distinct from \( x' \) and \( y' \).
Usage of this theorem is discouraged because it depends on [ax-13]. See
equvinv for a shorter proof requiring fewer axioms when \( z \) is
required to be distinct from \( x' \) and \( y' \). (Contributed by NM,
10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof
shortened by Wolf Lammen, 16-Sep-2023.) (New usage is discouraged.)
Conclusion
\( \vdash x' = y' \rightarrow \exists z \, (x' = z \wedge z = y') \)
Proof
l0
equtr
equcomi
l2
jctild l0 _
\( \vdash z = x' \rightarrow x' = y' \rightarrow x' = z \wedge z = y' \)
19.8a
\( \vdash x' = z \wedge z = y' \rightarrow \exists z \, (x' = z \wedge z = y') \)
l4
syl6 l2 _
\( \vdash z = x' \rightarrow x' = y' \rightarrow \exists z \, (x' = z \wedge z = y') \)
l5
ax13
\( \vdash \neg z = x' \rightarrow x' = y' \rightarrow \forall z \, x' = y' \)
ax6e
\( \vdash \exists z \, z = x' \)
eximii _ l2
19.35i _
\( \vdash \forall z \, x' = y' \rightarrow \exists z \, (x' = z \wedge z = y') \)
syl6 l5 _
\( \vdash \neg z = x' \rightarrow x' = y' \rightarrow \exists z \, (x' = z \wedge z = y') \)
pm2.61i l4 _