blob: 43ef06fb2cadd07a09289f05b080fb80a1e8ef99 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
\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}
|