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

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

/\ 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