Nuprl Definition : all-class-values+

all-class-values+{i:l}(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\}(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_56_16 Last ObjectModification: 2011_06_21-PM-02_44_27 Home Index