:: Axioms of Tarski {G}rothendieck Set Theory :: by Andrzej Trybulec :: :: Received January 1, 1989 :: Copyright (c) 1990-2018 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 :: TARSKI_0:1 for x being object holds x is set; :: Extensionality axiom theorem :: TARSKI_0:2 (for x being object holds x in X iff x in Y) implies X = Y; :: Axiom of pair theorem :: TARSKI_0:3 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 :: TARSKI_0:4 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 :: TARSKI_0:5 x in X implies ex Y st Y in X & not ex x st x in X & x in Y; :: Fraenkel's scheme scheme :: TARSKI_0:sch 1 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;