reg - Metamath Proof Explorer (original) (raw)

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 9241) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9242). A stronger version that works for proper classes is proved as zfregs 9378. (Contributed by NM, 14-Aug-1993.)