summaryrefslogtreecommitdiff
path: root/test/phase5/exact-replacement.tex
blob: d23ba4214a208e36913c6d00014fbd0da89c4fc6 (plain)
1
2
3
4
5
6
7
8
9
10
11
\begin{definition}\label{phase5_replacement_definition}
    $\phasefivereplacement{A} = \{ y \mid x \in A, y \in x \mid x = y \}$.
\end{definition}

\begin{proposition}\label{phase5_replacement_theorem}
    For all $A, x$ we have if $x \in A$, then $x \in \{ y \mid y \in A \}$.
\end{proposition}
\begin{proof}
    Fix $A, x$.
    Assume $x \in A$.
\end{proof}