Nuprl Lemma : vr_AC1p

vr_AC1p

'

Proof not projected

Definitions occuring in Statement : vr_AC1p: vr_AC1p, member: t

T, universe: Type
Definitions : isect:

x:A. B[x], uall:

[x:A]. B[x], function: x:A

B[x], all:

x:A. B[x], universe: Type, prop:

, apply: f a, product: x:A

B[x], exists:

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

Q, so_lambda:

x.t[x], member: t

T, equal: s = t, vr_AC1p: vr_AC1p, lambda:

x.A[x]
Lemmas : uall_wf

vr\_AC1p \mmember{} \mBbbU{}' Date html generated: 2012_02_20-PM-03_33_29 Last ObjectModification: 2012_02_02-PM-01_55_21 Home Index