Theorem 2ax6e

We can always find values matching \( x \) and \( y \), as long as they are represented by distinct variables. Version of 2ax6elem with a distinct variable constraint. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.)

Conclusion
\( \vdash \exists z \, \exists w \, (z = x \wedge w = y) \)
Proof
l0
aeveq
aeveq
jca l0 _
19.8ad _
l4
19.8ad _
\( \vdash \forall w \, w = z \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
2ax6elem
\( \vdash \neg \forall w \, w = z \rightarrow \exists z \, \exists w \, (z = x \wedge w = y) \)
pm2.61i l4 _