:: Axioms of Tarski {G}rothendieck Set Theory :: by Andrzej Trybulec :: :: Received January 1, 1989 :: Copyright (c) 1990-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ begin reserve x,y,z,a for object; reserve X,Y,Z for set; :: Set axiom theorem for x being object holds x is set; :: Extensionality axiom theorem (for x being object holds x in X iff x in Y) implies X = Y; :: Axiom of pair theorem for x,y being object ex z being set st for a being object holds a in z iff a = x or a = y; :: Axiom of union theorem for X being set ex Z being set st for x being object holds x in Z iff ex Y being set st x in Y & Y in X; :: Axiom of regularity theorem x in X implies ex Y st Y in X & not ex x st x in X & x in Y; :: Fraenkel's scheme scheme Replacement { A() -> set, P[object, object] }: ex X st for x holds x in X iff ex y st y in A() & P[y,x] provided for x,y,z being object st P[x,y] & P[x,z] holds y = z proof thus thesis; end;