Is there any epsilon delta proof, in which we use the bare minimum of $\delta $ existing? In every epsilon delta proof I see, it ends up with reverse engineering the epsilon inequality to find a suitable delta. Ultimately, it seems so that one can always write down $\delta$ as a function of $\epsilon$. What I want to know is, does there exist any epsilon delta proof, in which we can only show that the delta only exists (as is the minimum condition in the statement) rather than the explicit relation of it with epsilon?
I am of opinion that there may exist no such proof. If the answer to the previous question is there exists no known ones, why not just keep it in the statement of epsilon delta limit that "$\delta$ can be written as some function of $\epsilon $
, $\delta=f(\epsilon)$ with $f: \mathbb{R^+} \to \mathbb{R^+}$ "
 A: I think there is no real conceptual difference between the existence
of a $\delta_\epsilon$-function and the standard: For all $\epsilon$ there exists $\delta>0$ s.t...
There is, however, a subtle difference between 'you may find' / 'there exists'.
In a typical phrase regarding $\epsilon,\delta$ it reads
something like: Given any $\epsilon>0$ 'you may find' / 'there exists' $\delta>0$ such that ...
But there is also usually a monotonicity issue behind the curtain: If $\delta_0>0$ works for a given $\epsilon_0>0$ then $\delta_0$  also works for any $\epsilon>\epsilon_0$ and similarly any $0<\delta<\delta_0$ would work for the value $\epsilon_0$.
Assuming this monotonicity, to construct a $\delta(\epsilon)$ function you need induction but not AoC. It suffices to look at $\epsilon_k=1/k$, $k\geq 1$ and get ('find'/'there exists') a corresponding $\delta'_k>0$. Let $\delta_k=\min\{\delta'_1,\cdots,\delta'_k\}>0$. Then $\delta(\epsilon)=\max\{\delta_k :  k>1/\epsilon\}$ should do.
So the equivalent statement for this $\delta$ function would be:
'You may find' / 'There exists' a monotone decreasing function $\delta : \epsilon \in (0,+\infty) \to \delta_\epsilon\in (0,+\infty)$ with $\lim_{\epsilon\to 0^+} \delta_\epsilon=0$ such that...
Thus, I think the real underlying question persists also when thinking in terms of such a function. Can you actually construct such  function, or do you only know it exists?
For example: Perhaps it is consistent with ZF to assume that for every continuous function on the reals
one may construct such a $\delta$-function and then
all standard analysis (without AoC) works. Perhaps within ZFC you could construct an abstract function for which it is not possible to construct such a $\delta$ function? Frankly, I have no idea as to the answer of these two questions.
A: When proving that every real polynomial of a single variable is continuous as a function $\mathbf R \to \mathbf R$, you induct on the degree of the polynomial and rely on continuity of addition and multiplication as mappings $\mathbf R^2 \to \mathbf R$, but you don't rely on an "explicit relation" of $\delta$ in terms of $\varepsilon$ since that would be a big mess and quite distracting from the real ideas in the proof.
A: There are already a variety of good comments and answers from different points of view; I would like to present another perspective, and provide further details.


does there exist any epsilon delta proof, in which we can only show that the delta only exists (as is the minimum condition in the statement) rather than the explicit relation of it with epsilon?

No, as you guessed; (disregarding foundational issues that are bound to pop up eventually) any $\forall\epsilon,\exists\delta$ statement can be in principle turned into a more explicit relation between $\epsilon$ and $\delta$. Of course, in general how explicit the original setup is bounds from above how explicit this relation could be. Indeed, as discussed at Any function with a modulus of continuity proportional to any preassigned $\epsilon>0$ is Lipschitz-continuous, any $\forall\epsilon,\exists\delta$ is equivalent (disregarding foundations) to some  $\exists\delta,\forall\epsilon$, at the cost of a jump in the type of $\delta$; more explicitly
$$[\forall\epsilon\in\mathbb{R}_{>0},\exists\delta\in\mathbb{R}_{>0}: P(\epsilon,\delta)\text{ is true }]  \iff [\exists \delta\in F(\mathbb{R}_{>0};\mathbb{R}_{>0}),\forall \epsilon\in\mathbb{R}_{>0}: P(\epsilon,\delta(\epsilon)) \text{ is true}].$$
(In this context such a function $\delta$ is not unique; in contexts in which it is unique, $(\implies)$ with uniqueness is an implicit function theorem.)
More generally (in principle) one can convert (disregarding foundations) any
$$\forall \alpha\in A,\forall x_\alpha\in X_\alpha,\exists y\in Y: P(\{x_\alpha\}_{\alpha\in A},y)\text{ is true }$$
to a
$$\exists y\in F\left(\prod_{\alpha\in A}X_\alpha;Y\right),\forall \alpha\in A,\forall x_\alpha\in X_\alpha: P(\{x_\alpha\}_{\alpha\in A},y(\{x_\alpha\}_{\alpha\in A}))\text{ is true }.$$


why not just keep it in the statement of epsilon delta limit that "$\delta$ can be written as some function of $\epsilon $
, $\delta=f(\epsilon)$ with $f: \mathbb{R^+} \to \mathbb{R^+}$ "

This has to do with the scope and use of the statement to be written, which are ultimately based on personal preferences. For instance in the link above a uniform modulus of continuity for a function $f:X\to Y$ between metric spaces is defined as a function $\mathfrak{m}:\mathbb{R}_{>0}\to\mathbb{R}_{>0}$; however one could just as well define a modulus of continuity as a  function $\mathfrak{m}:C^0_u(X;Y)\times \mathbb{R}_{>0}\to \mathbb{R}_{>0}$ such that for any $f\in C^0_u(X;Y)$, for any $\epsilon\in\mathbb{R}_{>0}$, and for any $x_1,x_2\in X$:
$$d_X(x_1,x_2)< \mathfrak{m}(f,\epsilon)\implies d_Y(f(x_1),f(x_2))<\epsilon.$$
(This perspective is useful e.g. when talking about equicontinuity.)
(Here $C^0_u$ is the collection of uniformly continuous functions.)
Another alternative is to consider $X$ and $Y$ as metrizable spaces. Define $\widehat{C^0_u}(X;Y)$ as the set of triples $(d_X,d_Y,f)$ such that $d_X$ is a distance function on $X$ compatible with the topology of $X$, $d_Y$ is a distance function on $Y$ compatible with the topology of $Y$, and $f:X\to Y$ is uniformly continuous w/r/t $(d_X,d_Y)$. Then one can define a modulus of continuity as a function $\mathfrak{m}:\widehat{C^0_u}(X;Y)\times \mathbb{R}_{>0}\to \mathbb{R}_{>0}$ such that for any $(d_X,d_Y,f)\in\widehat{C^0_u}(X;Y)$, for any $\epsilon\in\mathbb{R}_{>0}$, and for any $x_1,x_2\in X$:
$$d_X(x_1,x_2)< \mathfrak{m}(d_X,d_Y,f,\epsilon)\implies d_Y(f(x_1),f(x_2))<\epsilon.$$
(This perspective, although somewhat in jest, is useful when there are different distances involved. For instance if $f:X\to \mathbb{R}$ is $\theta$-Hölder with respect to a distance function $d:X\to X\to\mathbb{R}_{\geq0}$, then it is Lipschitz with respect to the distance function $d^\theta:(x_1,x_2)\mapsto d(x_1,x_2)^\theta$, i.e. $\mathfrak{m}(d,f,\epsilon)=\left(\dfrac{\epsilon}{C}\right)^{1/\theta} \implies \mathfrak{m}\left(C d^\theta,f,\epsilon\right)=\epsilon$; see the discussion at the above link; Semmes calls the operation $d\mapsto d^\theta$ the "snowflake functor"; see the reference at Exponents for Hölder functions on metric spaces . Note that pointwise moduli of continuity can be considered to be better suited for this "fixed topology, different distances" perspective.)
(Yet another alternative is to define a modulus of continuity as a function $\mathfrak{m}: \operatorname{Arr}(\operatorname{Met}_u)\times \mathbb{R}_{>0}\to \mathbb{R}_{>0}$, where $\operatorname{Arr}(\operatorname{Met}_u)$ is the collection (category) of all uniformly continuous functions from a metric space to another one...)

Of course it is rude to deconstruct/universalize/invariantize some concept if it's not absolutely necessary for what is to come. E.g. in hyperbolic dynamics certain objects are automatically continuous, almost never differentiable, but to further the theory one needs something more than continuity (see Why Do We Care About Hölder Continuity?). In general, areas like dynamics where matters like stability, approximation, perturbation and deformation naturally introduce more moving parts.
The discussion at Difference between soft analysis and hard analysis is also somewhat relevant.

Finally, to contextualize some of the comments above, fix a function $f:X\to Y$ between metric spaces, and define its "uniform $\epsilon-\delta$ bundle" as
$$E(f)=\{(\epsilon,\delta)\in\mathbb{R}_{>0}^2\,|\, \forall x_1,x_2\in X: d_X(x_1,x_2)<\delta\implies d_Y(f(x_1),f(x_2))<\epsilon\}$$
with (a priori partially defined; Notation for "function from a subset of $X$ into $Y$"? ) projection $\pi:E(f)\rightsquigarrow \mathbb{R}_{>0}$ onto the first coordinate. Then ($\pi$ is defined everywhere and) there is a global section of $\pi:E(f)\to \mathbb{R}_{>0}$  iff $f$ is uniformly continuous, and existence of such a global section is equivalent to the axiom of choice (see https://ncatlab.org/nlab/show/axiom+of+choice), if each fiber is nonempty. Note that with this framework, if there is a section $\delta: \mathbb{R}_{>0}\to E(f)$, any other function $\delta':\mathbb{R}_{>0}\to\mathbb{R}_{>0}$ whose graph is under the graph of $\delta$ will also be a section. Due to other inequalities needed in a given argument one may have a lower bound $\sigma: \mathbb{R}_{>0}\to\mathbb{R}_{>0}$ also, and it might be important, for what is to come, to establish not only a section $\delta$ that stays above $\sigma$, but also one that is measurable/continuous/differentiable etc.. It's clear that this framework too can be universalized in variety of ways.
(Although, as a disclaimer this framework is somewhat misleading; as one can often focus on countably many values for $\epsilon$ (and $\delta$) (in which case countable choice would be sufficient to produce a section), so that the geometry $\pi:E(f)\to \mathbb{R}_{>0}$ seems to suggest is quite flexible.)
A: Answer in response to this comment from the OP on the excellent answer from
@KCd .

I am asking, one
where we only know that it exists behind the curtains. I ask this
because I want to make sure it is alright to say that we are just
finding a delta as a function of epsilon when doing the proof.

Whether or not that's OK depends on the context. For a graduate student or a professional mathematician, certainly. In an undergraduate course, perhaps. If the point of the question is to determine whether you can find an epsilon explicitly, then no. If the instructor or the text regularly says things like "this has been done before, no need to look behind the curtain" then yes.
When I ask my students for proofs, what I want to know is that they have convinced themselves for good reasons. How much handwaving is permitted depends on the level of the course and the student.
(When I was an undergraduate taking advanced calculus from Lars Ahlfors he informed us in the first class that he did not like proofs that reasoned from the hypotheses to some point, then back from the conclusion to the same point, and wrote "therefore" where the arguments met.)
