Theorem 2ax6elem
We can always find values matching \( x \) and \( y \), as long as they are
represented by distinct variables. This theorem merges two ax6e
instances \( \exists z \, z = x \) and \( \exists w \, w = y \) into a common expression.
Alan Sare contributed a variant of this theorem with distinct variable
conditions before, see [ax6e2nd]. Usage of this theorem is discouraged
because it depends on [ax-13]. (Contributed by Wolf Lammen,
27-Sep-2018.) (New usage is discouraged.)
Conclusion
\( \vdash \neg \forall w \, w = z \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
Proof
l0
ax6e
\( \vdash \exists z \, z = x \)
l1
hbnaev
\( \vdash \neg \forall w \, w = z \rightarrow \forall z \, \neg \forall w \, w = z \)
l1a
nf5i _
l2
nfnae
l3
nfan l1a _
l4
nfeqf
\( \vdash \neg \forall w \, w = z \wedge \neg \forall w \, w = x \rightarrow \Finv w \, z = x \)
l5
pm3.21
\( \vdash w = y \rightarrow z = x \rightarrow z = x \wedge w = y \)
l6
spimed l4 _
l7
eximd l3 _
\( \vdash \neg \forall w \, w = z \wedge \neg \forall w \, w = x \rightarrow \exists z \, z = x \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
l8
mpi l0 _
l9
ex _
\( \vdash \neg \forall w \, w = z \rightarrow \neg \forall w \, w = x \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
l10
ax6e
\( \vdash \exists z \, z = y \)
l11
nfae
l12
equvini
\( \vdash z = y \rightarrow \exists w \, (z = w \wedge w = y) \)
l13
equtrr
l14
anim1d _
l15
aleximi _
\( \vdash \forall w \, w = x \rightarrow \exists w \, (z = w \wedge w = y) \rightarrow \exists w \, (z = x \wedge w = y) \)
l16
syl5 l12 _
l17
eximd l11 _
\( \vdash \forall w \, w = x \rightarrow \exists z \, z = y \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
l18
mpi l10 _
\( \vdash \forall w \, w = x \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
l19
pm2.61d2 l9 _