# How the $EX(f)$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs.

I was trying to understand how the below would have executed step by step.

$$\exists_{f({v'})}[\,\underbrace{f({v'})}_\text{ROBDD of set of states}\,\land\, \underbrace{R({v}, {v'})}_\text{ROBDD of transition relation}\,]$$

So here the $f(v')$ is in ROBDD form and $R({v}, {v'})$ is also given in ROBDD form and now the $\land$ operation is performed on two ROBDDs , that I know how to perform. But where I stuck was

1. How does the there exists will be evaluated $\exists_{f(v')}$ after you get the resultant ROBDD of $f(v') \land R({v}, {v'})$ ?
2. After you perform the above operation you'll finally get some ROBDD representing the set of states, so from that set of states how will I get back the list of states ?