---

Step * of Lemma classrel-classfun

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)].  ∀[e:E]. ∀[v:T].  uiff(v ∈ X(e);v = X(e) ∈ T) supposing X is functional
BY
{ (Auto
   THEN DupHyp 5
   THEN D -1
   THEN RepeatFor 2 ((With ⌜e⌝ (D (-2))⋅ THENA Auto))
   THEN Try ((BHyp (-2) THEN Auto))
   THEN Try ((HypSubst (-3) 0 THEN Auto))
   THEN Thin (-3)
   THEN Unfold `classrel` 0
   THEN BLemma `bag-member-classfun`
   THEN Auto) }

---

Latex:

---

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  X  is  functional


By

---

Latex:
(Auto
  THEN  DupHyp  5
  THEN  D  -1
  THEN  RepeatFor  2  ((With  \mkleeneopen{}e\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto))
  THEN  Try  ((BHyp  (-2)  THEN  Auto))
  THEN  Try  ((HypSubst  (-3)  0  THEN  Auto))
  THEN  Thin  (-3)
  THEN  Unfold  `classrel`  0
  THEN  BLemma  `bag-member-classfun`
  THEN  Auto)

---

Home Index