Axiom the0 | index | src |

The negative case of definite description: if A is not a singleton then the A = 0.

axiom the0 {x y: nat} (A: set): $ ~E. y A == {x | x = y} -> the A = 0 $;