 as a substitute for \(X=Y\). The advantage of taking \(X=Y\) as a basic atomic formula would be that using (\ref{XY}) brings along extra quantifiers. Sometimes it is interesting to minimize the number of quantifiers in a formula. Also, (\ref{XY}) gives the identity \(X=Y\) an extensional flavour in contrast to a possibly different intensional construal. 