:: Axioms of Tarski {G}rothendieck Set Theory
::  by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 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;