[isabelle] set comprehension with pairs


Given  P :: 'a => 'b => bool, 

I would like to know what does the expression 

{(x,y). P x y} 

*precisely* stand for. 

Is it something like 

{z. EX x y. z = (x,y) /\ P x y} ?

Knowing this would help me deal more easily with some trivial set theory that seems reluctant to blasting.  I would also appreciate if someone showed me not only the answer to this, but also the way I could have found out myself looking at the online libraries.  

Thank you in advance, 
   Andrei Popescu 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.