Notation for there exists and let I sometimes encounter proofs as the following:

$\exists n\in\mathbb N$ such that …. Then $n$…

But the fact in that $n$ is not defined in the second sentence. A correct proof would contain instead:

$\exists n\in\mathbb N$ such that …. Let such a $n$. Then $n$…

Is there a notation to mean &quot;there exists and let&quot;?
You are asking about notation for &quot;there exists and let&quot;. Note that the first part of this, &quot;there exists,&quot; is a statement telling how something is, while &quot;let&quot; is an imperative telling the reader what to do. They have different roles in the proof and they have somewhat different formal languages.
The formal notation of statements contains things like quantifiers ($\forall,\ \exists$) and implications ($\implies$), while the formal notation for a proof rather is a deduction tree containing statements:
$$
\dfrac
{
  \begin{matrix}\\A \lor B\end{matrix}
  \quad
  \begin{matrix}\\ [A]\end{matrix}
  \quad
  \dfrac{[B] \quad B \rightarrow A}{A}
}
{
  A
}
$$
(The example proves $A$ from $A \lor B$ and $B \rightarrow A.$)
In a proof, &quot;there exists&quot; will be true either by some definition or by some other theorem or lemma, and the text would read &quot;By definition/theorem $X,$ there exists $x$ such that $P(x).$ Take such an $x.$ Then ...&quot; Here's a deduction tree for that:
$$
\dfrac
{
  \begin{matrix}\\ \triangledown \\ \hline \exists x\ P(x)\end{matrix}
  \quad
  \begin{matrix} [P(x)] \\ \vdots \\ Q \end{matrix}
}
{
  Q
}
$$
where $\triangledown$ denotes &quot;definition/theorem $X$&quot; and $\vdots$ that there is some deduction tree deriving $Q$ from $P(x).$ The left part above the horizontal line corresponds to &quot;By definition/theorem $X,$ there exists $x$ such that $P(x),$ and the right part corresponds to &quot;Take such an $x.$ Then $P(x)$ so ... Thus $Q(x).$&quot;
In $(\exists x \in X)R(x)$ in $R(x)$ $x$ is actually defined, because it is same as $(\exists x) (x \in X \land R(x))$.
Addition.
If we consider $(\exists x \in X)R(x) \land S(x)$, then it same as $(\exists y \in X)R(y) \land S(x)$.