Def  x:A st P(x)B(x) == x:{x:A| P(x) }B(x)

is not otherwise mentioned in this or prior sections.

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html