:: Axioms of Tarski {G}rothendieck Set Theory
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

:: Set axiom

theorem :: TARSKI_0:1

for x being object holds x is set ;

:: Extensionality axiom

theorem :: TARSKI_0:2

for X, Y being set st ( for x being object holds
( x in X iff x in Y ) ) holds
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

for x being object
for X being set st x in X holds
ex Y being set st
( Y in X & ( for x being object holds
( not x in X or not x in Y ) ) ) ;

:: Fraenkel's scheme

scheme :: TARSKI_0:sch 1
Replacement{ F₁() -> set , P₁[ object , object ] } :

ex X being set st
for x being object holds
( x in X iff ex y being object st
( y in F₁() & P₁[y,x] ) )

provided

for x, y, z being object st P₁[x,y] & P₁[x,z] holds
y = z

proof end;