w of u which is disjoint from u. Since w is in u, w is unranked. w is a subset of t by the definition of transitive closure. Since w is disjoint from u, every element of w is ranked. Applying the axioms of replacement and union to combine the ranks of the elements of w, we get an ordinal rank for w, to wit . This contradicts the conclusion that w is unranked. So the assumption that u was non-empty must be false and x must have rank. For every two sets, only one can be an element of the other Let X and Y be sets. Then apply the axiom of regularity to the set {X,Y} (which exists by the axiom of pairing). We see there must be an element of {X,Y} which is also disjoint from it. It must be either X or Y. By the definition of disjoint then, we must have either Y is not an element of X or vice versa. The axiom of dependent choice and no infinite descending sequence of sets implies regularity Let the non-empty set S be a counter-example to the axiom of regularity; that is, every element of S has a non-empty intersection with S. We define a binary relation R on S by , which is entire by assumption. Thus, by the axiom of dependent choice, there is some sequence (an) in S satisfying anRan+1 for all n in N. As this is an infinite descending chain, we arrive at a contradiction and so, no such S exists. Regularity and the rest of ZF(C) axioms Regularity was shown to be relatively consistent with the rest of ZF by and , meaning that if ZF without regularity is consistent, then ZF (with regularity) is also consistent. For his proof in modern notation see for instance. The axiom of regularity was also shown to be independent from the other axioms of ZF(C), assuming they are consistent. The result was announced by Paul Bernays in 1941, although he did not publish a proof until 1954. The proof involves (and led to the study of) Rieger-Bernays permutation models (or method), which were used for other proofs of independence for non-well-founded systems ( and ). Regularity and Russell's paradox Naive set theory (the axiom schema of unrestricted comprehension and the axiom of extensionality) is inconsistent due to Russell's paradox. In early formalizations of