theorem

for

X,

Y being

set st ( for

x being

object holds

(

x in X iff

x in Y ) ) holds

X = Y ;

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 ) ) ;

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 ) ) ;

theorem

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 ) ) ) ;

scheme

Replacement{

F_{1}()

-> set ,

P_{1}[

object ,

object ] } :

ex

X being

set st

for

x being

object holds

(

x in X iff ex

y being

object st

(

y in F_{1}() &

P_{1}[

y,

x] ) )

provided
for

x,

y,

z being

object st

P_{1}[

x,

y] &

P_{1}[

x,

z] holds

y = z