How do we formalize "such that"? How do we formally express the statement "$S$ is the set of natural numbers such that $P_n$ is true."?
Do we write "$n$ is an element of $S$ iff $n$ is an element of $\mathbb{N}$ and $P_n$" or "$n$ is an element of $S$ iff $n$ is an element of $\mathbb{N}$ then $P_n$"?
 A: I think that "$S$ is the set of natural numbers $n$ such that $P_n$ is true" is formal enough for most purposes. You could also write "$S$ is the set defined by $n \in S$ iff $n \in \mathbb{N}$ and $P_n$," which makes sense because, by the Axiom of Extensionality, a set is specified by giving a necessary and sufficient condition to be a member of that set.
The definition given by par, using "set builder" notation, is also common.  However, it's not really any more formal, even though it involves more symbols.  By this I mean that the ZFC axioms alone do not specify a meaning for $S \equiv \{n \in \mathbb{N} \mid P_n\}$.
A: Let $S$ be the set of natural numbers s.t. $P_n$ is true. In ZF(C), the axiom of specification dictates that $S$ exists (https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory#3._Axiom_schema_of_specification_.28also_called_the_axiom_schema_of_separation_or_of_restricted_comprehension.29).
Formally, you would write
$$S \equiv \left \{ n \in \mathbb{N} \mid P_n \right \}$$
which is closer to your first suggestion except that we begin by restricting $n$ to the set $\mathbb{N}$ instead of just saying
$$S \equiv \left \{ n \mid n \in \mathbb{N} \wedge P_n \right \}.$$
Addition: Note that we begin by restricting $n$ to be a member of $\mathbb{N}$, as that is how the axiom of specification is written. Of course, you could ask yourself, "Why do we have to restrict $n$ to any set to begin with?" If you find yourself asking this and are not content with the take-it-as-is approach to the ZF(C) axioms, I would read about Russel's paradox (https://en.wikipedia.org/wiki/Russells_paradox). There is a particularly nice and easy to follow introduction on the paradox in Paul Halmos' Naive Set Theory (https://en.wikipedia.org/wiki/Naive_Set_Theory_(book)).
A: 
Do we write "$n$ is an element of $S$ iff $n$ is an element of $\mathbb{N}$ and $P_n$" 

You could also write this as 
$\forall n (n\in S \iff (n\in N \land P(n))$
This would be correct.

or "$n$ is an element of $S$ iff $n$ is an element of $\mathbb{N}$ then $P_n$"?

Assuming you mean 
$\forall n(n\in S\iff(n\in N \implies P(n))) $
or equivalently
$\forall n(n\in S\iff(n\notin   N \lor P(n))) $
It would then follow that 
$\forall n(n\notin  N \implies n\in S) $
I don't think you want that.
