If you need the element elsewhere in the definition of the action that removes it from the set, you can write
LET e == CHOOSE x \in set : TRUE
IN /\ set' = set \ {e}
/\ \* remainder of the action
If you need e in a different action later in the execution, you will need to represent it as a state variable and you can write
/\ e' = CHOOSE x \in set : TRUE
/\ set' = set \ {e}
/\ ...
Note that CHOOSE picks an arbitrary but fixed element from the set: if the set contains {1,2,3} then TLC will generate one successor state in which the chosen element (say, 1) has been removed.
If you wish to model check your system for all possible choices of elements, use an existential quantifier as in
\E e \in set : set' = set \ {e}
In the above example, TLC will explore three successor states corresponding to removing each of the elements.
Stephan