@famesyasd Indeed you can consider them to be so! Specifically, "{a}" can be considered as a syntactic short-hand for "s1(a)" where "s1" is a 1-input function-symbol defined by applying definitorial expansion to the theorem "∀x ∃!y ∀e ( e∈y ⇔ e=x )".
That plus definitorial expansion allows you to introduce the new symbol "s1" along with an axiom "∀x ∀y ( s1(x) = y ⇔ ∀e ( e∈y ⇔ e=x ) )".
And that axiom turns out to be equivalent to "∀x ∀e ( e∈s1(x) ⇔ e=x )".
okay, how do I manipulate them? I mean {a} as a whole, that is a function-symbol and variables in it, like ordinary constants and variables? say, can I deduce in the proof that {a} = {a} (given a)?
ah okay
so formulas with function-symbols in them should act like when I had formulas with predicat-symbols
@famesyasd Since "{a}" is short-hand for "s1(a)", it is a term, and so trivially you can deduce "{a} = {a}". And because it's a term, you can form other terms like "{{{a}}}". (In any context where a is defined.)
You will have a slight problem. It is not defined if A is empty, so to force it into ZFC plus standard first-order logic you will have to use an unnatural trick, the same kind one needs to define division over the field axioms.
Let me do the field one, so that the logic issues are clearer.
Let's just do it for reals.
We start with the theorem "∀x∈R ( x≠0 ⇒ ∃!y∈R ( x·y = 1 ) )".
This is not of the form needed to perform definitorial expansion. So how? The only way is to force it by 'defining' the inverse of 0. We can choose anything, so for fun let's choose 13.
The theorem now becomes "∀x∈R ∃!y∈R ( x=0 ∧ y=13 ∨ x≠0 ∧ ( x·y = 1 ) )".
With this you can add a new function symbol, say "i", and the axiom:
