:: Axioms of Tarski {G}rothendieck Set Theory
:: by Andrzej Trybulec
::
:: 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{ F1() -> set , P1[ object , object ] } :
ex X being set st
for x being object holds
( x in X iff ex y being object st
( y in F1() & P1[y,x] ) )
provided
for x, y, z being object st P1[x,y] & P1[x,z] holds
y = z
proof end;