\begin{axiom}\label{phase5_relational_support}
    For every set $A$ we have $A = A$.
\end{axiom}

\begin{definition}\label{phase5_relational_replacement_definition}
    $\phasefiverelational{A} = \{ y \mid \exists x\in A. y = x \}$.
\end{definition}

\begin{proposition}\label{phase5_relational_replacement_local}
    For every set $A$ we have $A = A$.
\end{proposition}
\begin{proof}
    Fix $A$.
    Let $B = \{ y \mid \exists x\in A. y = x \}$.
    Follows.
\end{proof}