---

Step * of Lemma classrel-classfun-res-alt1

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e:E]. ∀[v:T].
  uiff(v ∈ X(e);if e ∈b X then v = X@e ∈ T else False fi ) 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);if e ∈b X then v = X@e ∈ T else False fi )

2
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)
8. z : v ∈ X(e)
9. x : Unit@i
⊢ ↑e ∈b X

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

---

Latex:


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


By

(UnivCD\mcdot{}  THENA  Auto)

---

Home Index