---

Step * of Lemma classfun-res_wf

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e:E].
  (X@e ∈ T) supposing (single-valued-classrel(es;X;T) and (↑e ∈b X))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``classfun-res classfun`` 0
   THEN Auto
   THEN Try (ProveSingleVal)
   THEN RWO "member-eclass-iff-size" (-2)
   THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``classfun-res  classfun``  0
  THEN  Auto
  THEN  Try  (ProveSingleVal)
  THEN  RWO  "member-eclass-iff-size"  (-2)
  THEN  Auto)

---

Home Index