How to extract an element from a set? Given for example $B=\{A\}$, how do you express $A$ in formal set theory? You'd be tempted to say "the unique element $X$ such that $X$ is a member of $B$", but the only way I know to express "such that" in set theory is with set builder notation:
$$\{X | X \in B\}$$
But this is useless since we've wrapped $A$ up inside a set once again.
This strikes me as an important question, since otherwise how can we express $f(x)$? You'd need something like "the second member of the ordered pair in $f$ whose first member is $x$", which is a more complicated version of the above problem.
 A: I have seen people write $\iota x Px$ to denote the unique $x$ satisfying $Px$.
However, I don't think its the best way of doing things. I'd much rather write:

Therefore, there exists a unique $x$ such that $Px$. Thus, let us adjoin a new constant symbol $c$ together with the assumption that $Pc$.

To make proper sense of the above paragraph, you should probably have a read of this and this.
Indeed, we can pull essentially same trick for functions.

Therefore, we have that for all $x$, there exists a unique $y$ such that $Pxy$. Thus, let us adjoin a new function symbol $f(*)$ together with the assumption that $\forall xy[f(x)=y \leftrightarrow Pxy].$

With regards to the "functions as particular kinds of sets" idea found in ZFC, we can define this as follows.

Therefore, we have that for all functions $f$ with domain $X$, and all $x \in X$, that there exists a unique $y$ such that $(x,y) \in f$. Thus, let us adjoin a new function symbol $* \diamond *$ together with the following sentence. 
For all $x$, $X$ and $f$, supposing $f$ has domain $X$ and that $x \in X$, then $f \diamond x = y \leftrightarrow (x,y) \in f.$
Indeed, we will write $f(x)$ rather than $f \diamond x$ whenever there is no scope for confusion.

Now if you're very switched on, you'll be wondering: "But hand on. My axiom schemata (like separation/replacement in ZFC, or first-order induction in PA) have an instance for each formula in my language. But, now that I've extended my language, what guarantee do I have that the schemata apply to the enlarged language?
But perhaps someone more knowledgeable than me can fill you in on that issue.
A: I have also thought of it. I call things like $f(x)$ a pseudo-object since it's an object + logical constraint. In the case that logical constraint is not satisfied, there is actually no object and the expression is undefined. Even if $f(x)$ may not be defined, all logical expressions containing it are perfectly defined. $y = f(x) \iff ⟨x, y⟩ ∈ f$ and $f$ is a function. It can be also defined in terms of your element extractor pseudoobject: $f(x) = El(f[\{x\}])$. Where $y ∈ El(x) \iff ∃z: (y ∈ z) ∧ (z = El(x))$ and $y = El(x) \iff (y ∈ x) ∧ (∀y') (y' ∈ x) \to (y' = y)$. Another example of construction like this is $X = A \dot∪ B $ meaning that $X$ is disjoint union of $A$ and $B$. Here $A \dot∪ B$ is pseudoobject of $A ∪ B$ + condition that $A ∩ B = ∅$.
