From a previous question it was confirmed that the equivalence:
$\forall x \forall y \bullet Overlap(x,y) \equiv (\exists z Part(z,y) \land Part(z,x)) \ $ (1)
could be transformed into the pair of implications:
$\forall x \forall y : (Overlap(x,y) \Rightarrow (\exists z : (Part(z,x) \land Part(z,y)))) \ $ (1a)
$\forall x \forall y : ((\exists z : Part(z,x) \land Part(z,y)) \Rightarrow Overlap(x,y)) \ $ (1b)
Is this transformation still valid if the sentence is definitional using definitional equality?
$\forall x \forall y \bullet Overlap(x,y) \stackrel{\mathrm{def}}{=} (\exists z Part(z,y) \land Part(z,x))\ $ (2)