Nuprl Definition : all-class-values

all-class-values{i:l}(Info;es;T;A;t.P[t]) ==

[e:E].

[t:T]. P[t] supposing t

A(e)

Proof not projected

Definitions occuring in Statement : classrel: v

X(e), es-E: E, uimplies: b supposing a, uall:

[x:A]. B[x]
Definitions : es-E: E, uall:

[x:A]. B[x], uimplies: b supposing a, classrel: v

X(e)
FDL editor aliases : all-class-values

all-class-values\{i:l\}(Info;es;T;A;t.P[t]) == \mforall{}[e:E]. \mforall{}[t:T]. P[t] supposing t \mmember{} A(e) Date html generated: 2011_10_20-PM-04_55_50 Last ObjectModification: 2011_06_21-PM-02_37_36 Home Index