Nuprl Definition : uall

This is "uniform" universal quantification.
Evidence for ⌜∀[x:A]. B[x]⌝ must be something that is member of ⌜B[x]⌝
whenever ⌜x ∈ A⌝Such evidence is independent of the choice of ⌜x ∈ A⌝. ⋅

[x:A]. B[x] ==  ⋂x:A. B[x]

Definitions occuring in Statement :  isect: x:A. B[x]
Definitions occuring in definition :  isect: x:A. B[x]
Rules referencing :  Continuity ispairCases isintCases isatomCases isaxiomCases islambdaCases isinlCases isinrCases isatom1Cases isatom2Cases lessCases uallFunctionality uallLevelFunctionality
FDL editor aliases :  uall

\mforall{}[x:A].  B[x]  ==    \mcap{}x:A.  B[x]

Date html generated: 2016_07_08-PM-04_46_30
Last ObjectModification: 2015_10_29-PM-07_09_51

Theory : core_2

Home Index