Translate the following inference to logic notation: For all x, x will play tennis if and only if x is a server. Mary is playing tennis. Therefore there is at least one x for which x is a server.
forall x: P(x) <-> Q(x). P(a). Therefore exists x: Q(x).