Nuprl Definition : single-valued-classrel

single-valued-classrel(es;X;T) ==  ∀e:E. ∀v1,v2:T.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ T))


Definitions occuring in Statement :  classrel: v ∈ X(e),  es-E: E,  all: ∀x:A. B[x],  implies: P ⇒ Q,  equal: s = t ∈ T
FDL editor aliases :  single-valued-classrel
single-valued-classrel(es;X;T)  ==    \mforall{}e:E.  \mforall{}v1,v2:T.    (v1  \mmember{}  X(e)  {}\mRightarrow{}  v2  \mmember{}  X(e)  {}\mRightarrow{}  (v1  =  v2))


Date html generated: 2015_07_17-PM-00_19_55
Last ObjectModification: 2012_02_25-PM-01_13_47

Home Index