Nuprl Definition : all-class-value-ordered-pairs+

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

[e1,e2:E]. (e1 c

e2

(

[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-causle: e c

e', es-E: E, uimplies: b supposing a, uall:

[x:A]. B[x], implies: P

Q
Definitions : es-E: E, implies: P

Q, es-causle: e c

e', uall:

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

X(e)
FDL editor aliases : all-class-value-ordered-pairs+

all-class-value-ordered-pairs+\{i:l\}(es;T;A;t1,t2.Q[t1; t2]) == \mforall{}[e1,e2:E]. (e1 c\mleq{} e2 {}\mRightarrow{} (\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_57_11 Last ObjectModification: 2011_06_21-PM-03_04_42 Home Index