Axiom theid | index | src |

The positive case of definite description: A = {a} then the A = a.

axiom theid {x: nat} (A: set) (a: nat): $ A == {x | x = a} -> the A = a $;