Suppose you're asked to give a formal proof of $\forall x \forall y(x \in \{x,y\})$, where a formal proof is essentially a sequence of invocations of inference rules and appeals to the set theory axioms. Assuming the inference rules of propositional logic and predicate logic are understood, what else do we need to establish to prove this? I guess what I'm saying is that I'm not sure how to manipulate the set literal (if you can call it that) notation. Is $\{x,y\}$ really just shorthand for something else that's easier to manipulate? Perhaps set literal notation is defined by something like "$x\in\{s_1,s_2,\dots,s_n\}$ is an abbreviation for $x=s_1 \vee x=s_2 \vee \dots \vee x=s_n$"? If that were the case, the proof would be very easy to write. So, is this how one would actually define the notation, or am I still missing something?
Note that my background in formal proofs comes from Graeme Forbes' "Modern Logic" and my past math teachers must have considered set literal notation intuitive enough that they didn't have to provide a definition of it as really being an abbreviation or something.
You asked, "Is $\{x,y\}$ really just shorthand for something else that's easier to manipulate?"
It's actually shorthand for something else that's harder to manipulate (because it's long and unwieldy).
A formula of the form $\varphi(\{x,y\})$ can be viewed as an abbreviation for
$$(\exists a)\Big(\varphi(a) \land (\forall b)\big(b\in a \iff (b=x\lor b=y)\big)\Big)$$
or for
$$(\forall a)\Big((\forall b)\big(b\in a \iff (b=x\lor b=y)\big)\implies \varphi(a)\Big),$$
which are equivalent over ZF (and, in fact, over much weaker set theories).