Tarski's axioms are an alternate formalization of geometry (similar to axiom sets of Euclid and later Hilbert). Do these axioms imply: $$\forall\; x,y\in \text{points},\; x x\equiv y y?$$
If yes, what is the proof? My feeling is that the proof must use Tarski's Identity of Congruence $$xy\equiv zz \rightarrow x = y,$$ but I am unable to find a proof.
On
Let $y$ and $v$ be arbitrary. Let $z=u=y$ and $w=v$. By the segment construction axiom, there exists $x$ such that $Bvyx$ and $yx=vy$. Then, the hypothesis of the axiom of Euclid (form A using the same letters as I have used here) is satisfied, so we conclude $yz\equiv vw$. But indeed $y=z$ and $v=w$ so we have $yy\equiv vv$. Since $y$ and $v$ were arbitrary, we conclude $\forall y\forall v (yy\equiv vv)$.
I implicitly used a couple facts without stating which you should try to prove. Namely, $Byyy$ is a tautology, and $Bvyx$ iff $Bxyv$.
On
You do not need Euclid's axiom nor five segments, using segment construction build a point $z$ such that Bet yxz and xz=yy. Using identity of congruence, we have x=z.
The machine checked proof of this results and many other is available in the GeoCoq library, it the lemma cong_trivial_identity line 72 here: https://github.com/GeoCoq/GeoCoq/blob/master/Tarski_dev/Ch02_cong.v
This seems surprisingly tricky. Identity of Congruence isn't enough by itself since it goes in the wrong direction.
I want to use the Five Segment Axiom. Let me call your two points $p,q$ instead, to avoid a conflict with Wikipedia's notation. If $p=q$ then we are done by reflexivity, so assume $p \ne q$. Set $u=z=x'=p$ and $u'=z'=x=q$. Let $y=y'$ be the midpoint of $pq$ (it takes some more work to prove that it exists), so $Bpyq$ and $py \equiv qy$. Now we verify that the hypothesis of the Five Segment Axiom is satisfied, and conclude $zu \equiv z'u'$ which is to say $pp \equiv qq$.