The negative case of definite description: if A is not a singleton then the A = 0.
A
the A = 0
axiom the0 {x y: nat} (A: set): $ ~E. y A == {x | x = y} -> the A = 0 $;