Step
*
of Lemma
singlevalued-graph_wf
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}. ∀x:coSet{i:l}. (singlevalued-graph(A;a.B[a];x) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}A:coSet\{i:l\}. \mforall{}B:\{a:coSet\{i:l\}| (a \mmember{} A)\} {}\mrightarrow{} coSet\{i:l\}. \mforall{}x:coSet\{i:l\}.
(singlevalued-graph(A;a.B[a];x) \mmember{} \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index