The positive case of definite description: A = {a} then the A = a.
A = {a}
the A = a
axiom theid {x: nat} (A: set) (a: nat): $ A == {x | x = a} -> the A = a $;