---

Step * of Lemma classrel-classfun-res

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

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

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

---

Latex:


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


By

((UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index