Description: Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also
called the Axiom of Foundation. A rather non-intuitive axiom that
denies more than it asserts, it states (in the form of zfreg ) that
every nonempty set contains a set disjoint from itself. One consequence
is that it denies the existence of a set containing itself ( elirrv ).
A stronger version that works for proper classes is proved as zfregs .
(Contributed by NM, 14-Aug-1993)