How to formally prove using first-order set theory that $\{7,8,9\}=\{7,8,10\}$ is a false statement? Consider $\{7,8,9\}$ and $\{7,8,10\}$ to be the informal representations of two sets. Formally, in naive first-order set theory, we define these sets as
$$\exists a\  \forall x\ (x \in a \iff (x=7 \lor x=8 \lor x=9))$$
$$\exists b\  \forall x\ (x \in b \iff (x=7 \lor x=8 \lor x=10))$$
How do we formally prove, using naive first-order set theory, that these sets are different?
Note that informally, I believe we could prove it thus:

From the Axiom of Comprehension and Axiom of Extensionality, we can
prove that for each well-formed formula P(x) in FOL, there is a unique
set of objects that satisfy P(x).
Let's assume this proof has already been given. Then since the objects
satisfying $P_1(x)=x=7 \lor x=8 \lor x=9$ are different from the objects
satisfying $P_2(x)=x=7 \lor x=8 \lor x=10$, the unique sets made of
objects satisfying each of these formulas are different.

Here is the line of reasoning of my incomplete attempt at a formal proof, using first-order logic:
I take the two definitions of the sets as premises. I start with a subproof by existential elimination, with the premise:

*

*Assume a is a set such that $\forall x\ (x \in a \iff (x=7 \lor x=8 \lor x=9))$.

Nested within, I start another subproof by existential elimination, with the premise:

*

*Assume b is a set such that $\forall x\ (x \in v \iff (x=7 \lor x=8 \lor x=10))$.

The Axiom of Extensionality says
$$\forall a\ \forall b\ [\forall x\ (x \in a \iff x \in b) \implies a=b]$$
By Universal Elimination, I can state
$$\forall x\ (x \in a \iff x \in b) \implies a=b\tag{1}$$
At this point, I have a material conditional, and I want to prove $a \neq b$.
If I assume $a=b$, $(1)$ doesn't actually let me do anything with this assumption. In fact, using just the two Axioms (Comprehension and Extensionality) $a=b$ doesn't seem to lead to any other statement that I can infer.
After all, it seems to be the case that $\forall x\ (x \in a \iff x \in b)$ can be false and $a=b$ true, since we don't have a biconditional (another source of doubt for me in this material).
Edit: What do I mean by FOL?
I learned what I imagine is a very basic form of FOL which includes introduction and elimination inference rules for $\land,\lor,\implies,\iff,\lnot$, quantifiers $\forall, \exists$, introduction and elimination inference rules for $\forall$ and $\exists$, plus the identity predicate.
When naive set theory was introduced to me, there was only one symbol, $\in$, the Axiom of Comprehension, and the Axiom of Extensionality.
Axiom of Comprehension
$$\exists a \forall [x \in a \iff P(x)]$$
Axiom of Extensionality
$$\forall a \forall b [\forall x (x \in a \iff x \in b) \implies a = b]$$
 A: You don't need extensionality to prove that $\{ 7, 8, 9 \} \neq \{ 7, 8, 10 \}$.$^*$ Simply observe that $9 \in \{7, 8, 9 \}$ but $9 \notin \{7, 8, 10 \}$, therefore $\{ 7, 8, 9 \} \neq \{ 7, 8, 10 \}$.
If you want to write this last step in more detail, you could say that if $9 \in \{ 7, 8, 9 \}$ and $\{ 7, 8, 9 \} = \{ 7, 8, 10 \}$, then $9 \in \{ 7, 8, 10 \}$, but this is false, hence $\{ 7, 8, 9 \} \neq \{ 7, 8, 10 \}$.
Edit: since you ask for a formal proof:

*

*$\forall x (x \in \{ 7, 8, 9 \} \leftrightarrow (x = 7 \vee x = 8 \vee x = 9))$.

*$\forall x (x \in \{ 7, 8, 10 \} \leftrightarrow (x = 7 \vee x = 8 \vee x = 10))$.

*$9 \in \{ 7, 8, 9 \}$. (By universal instantiation. Take $x = 9$ in 1.)

*$9 \notin \{ 7, 8, 10 \}$. (By universal instantiation. Take $x = 9$ in 2.)

*$\{ 7, 8, 9 \} = \{ 7, 8, 10 \} \rightarrow (9 \in \{ 7, 8, 9 \} \rightarrow 9 \in \{ 7, 8, 10 \})$. (This, or some equivalent formula, is an instance of an axiom of predicate logic with equality.)

*$\{ 7, 8, 9 \} \neq \{ 7, 8, 10 \}$. (By propositional logic.)

$^*$ Although if extensionality did not hold, then one could not make much sense of the notation $\{ 7, 8, 9 \}$ in the first place, since $\{ 7, 8, 9 \}$ is defined to be the unique set (unique by extensionality!) which contains the elements $7, 8, 9$ and nothing else.
A: We want to prove that $\{7,8,9\}=\{7,8,10\}$ is a false stetement.
Let's assume the premise is true.
We have $\forall x(x\in \{7,8,9\} \iff x\in \{7,8,10\})$, by definition.
This implies that $9\in \{7,8,9\} \iff 9\in \{7,8,10\}$. This is where we use the universal instantation which you mentioned in your post. Since the statement is true for ANY value of x, that means that substituting x with ANYTHING will still gice us a true statement. In this example, we have substitued x with 9.
$9=7 \lor 9=8 \lor 9=9 \iff 9=7 \lor 9=8 \lor 9=10$, using your own definition of an element being part of a set.
$false \lor false \lor true \iff false \lor false \lor false$
$true \iff false$
$false$
The premise leads to an impossible conclusion. From this we can conclude that the sets are indeed not equal.
A: First, let's investigate Axiom of Extensionality.
Axiom of Extensionality. For any two sets $A,B$,
\begin{equation}
(\text{for any }x\text{ we have }x\in A\text{ if and only if }x\in B)\Leftrightarrow A=B.
\end{equation}
In fact, Axiom of Extensionality is $\Rightarrow$ while $\Leftarrow$ follows the meaning of $=$. "$\Rightarrow$" is equivalent of say "If the extensions of $A$ and $B$ are the same then $A$ and $B$ are equal". "$\Leftarrow$" is equivalent to say "If $A$ and $B$ are equal then the extensions of $A$ and $B$ are the same" which is a truth in all the truth theory which is determined since if $A$ and $B$ are equal then everything of $A$ and $B$ are the same. Although of this, we usually combine the two arrows together since "$\Leftarrow$" is obvious.
Now turn to your problem. To show $\{7,8,9\}\neq\{8,9,10\}$ is easy that we just need to use "$\Leftarrow$" which is a truth while in fact not Axiom of Extentionality.
Proof 1. Suppose $\{7,8,9\}=\{8,9,10\}$. Since $7\in\{7,8,9\}$, then by $\{7,8,9\}=\{8,9,10\}$ we have $7\in\{8,9,10\}$, clearly contradicted to $7\notin\{8,9,10\}$.
Proof 2. Suppose $\{7,8,9\}=\{8,9,10\}$. Since $10\in\{8,9,10\}$, then by $\{7,8,9\}=\{8,9,10\}$ we have $10\in\{7,8,9\}$, clearly contradicted to $10\notin\{7,8,9\}$.
