How to choose a record field when a record is an element of a set?

[Y2i <yur...@xxxxxxxxx>]

Looking for a practical advice...

Let's assume I'm reading a record by its ID.  There is at most one record with such an ID.

TypeInvariant == \A d \in data : Cardinality({x \in data : x.id = d.id}) = 1

If such record exists, I need to return its d field.  I currently use CHOOSE to select such a record:

R(r) == CHOOSE x \in r : TRUE

Read(r) ==

    /\ r.op = "R"

    /\ LET d == {x \in data : x.id = r.id}

       IN  IF d = {} THEN

               qout' = Append(qout, [code|->"ERR"])

           ELSE

               qout' = Append(qout, [code|->"OK", d|->R(d).d])

    /\ UNCHANGED <<data>>

Is there a  better way to achieve this?

Thank you,

Yuri