From no assumptions derive the conclusion
∃x t = x
(where t can be any term).
Unless one is considering a "free logic", classical first order logic assumes all models that would be permitted to provide countermodels have a non-empty domain. So there exists a member of the domain which one may name t. Let x be a variable representing any member of the domain.
Here is a proof of the above using a Fitch-style proof checker:
The first line of the proof asserts that the domain is not empty. Equality introduction can derive the existence of t = t.
The next line uses existential introduction (∃I) on the second t of line 1 to derive the goal on line 2.
One may wonder why I was not forced by the proof checker to replace both instances of t with x when I used existential introduction. The authors of forallx explain it as follows: (Chapter 32, page 260)
But we do not need to replace both instances of a name with a variable: if Narcissus loves himself, then there is someone who loves Narcissus.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf