Nuprl Definition : all-class-value-pairs+

all-class-value-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]) ==

[e1,e2:E].

[t1,t2:T]. (Q[t1; t2]) supposing (t2

A(e2) and t1

A(e1))

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-value-pairs+

all-class-value-pairs+\{i:l\}(es;T;A;t1,t2.Q[t1; t2]) == \mforall{}[e1,e2:E]. \mforall{}[t1,t2:T]. (Q[t1; t2]) supposing (t2 \mmember{} A(e2) and t1 \mmember{} A(e1)) Date html generated: 2011_10_20-PM-04_56_44 Last ObjectModification: 2011_06_21-PM-02_53_02 Home Index