---

Step * of Lemma classrel-classfun-res-alt2

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e:E]. ∀[v:T].
  uiff(v ∈ X(e);(↑e ∈b X) ∧ (v = X@e ∈ T)) supposing single-valued-classrel(es;X;T)
BY
{ (UnivCD⋅ THENA Auto) }

1
1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. v : T
7. single-valued-classrel(es;X;T)
⊢ uiff(v ∈ X(e);(↑e ∈b X) ∧ (v = X@e ∈ T))

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].  \mforall{}[e:E].  \mforall{}[v:T].
    uiff(v  \mmember{}  X(e);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (v  =  X@e))  supposing  single-valued-classrel(es;X;T)


By

(UnivCD\mcdot{}  THENA  Auto)

---

Home Index