Universal quantification of negation is equivalent to negation of existential quantification. Dual of exnal (but does not depend on [ax-4] contrary to it). See also the dual pair [df-ex] / alex. Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)