let X be set ; :: thesis: for x being object st x in X holds

Class ((nabla X),x) = X

let x be object ; :: thesis: ( x in X implies Class ((nabla X),x) = X )

assume A1: x in X ; :: thesis: Class ((nabla X),x) = X

( y in X iff y in Class ((nabla X),x) ) ;

hence Class ((nabla X),x) = X by TARSKI:2; :: thesis: verum

Class ((nabla X),x) = X

let x be object ; :: thesis: ( x in X implies Class ((nabla X),x) = X )

assume A1: x in X ; :: thesis: Class ((nabla X),x) = X

now :: thesis: for y being object st y in X holds

y in Class ((nabla X),x)

then
for y being object holds y in Class ((nabla X),x)

let y be object ; :: thesis: ( y in X implies y in Class ((nabla X),x) )

assume y in X ; :: thesis: y in Class ((nabla X),x)

then [y,x] in nabla X by A1, ZFMISC_1:87;

hence y in Class ((nabla X),x) by Th19; :: thesis: verum

end;assume y in X ; :: thesis: y in Class ((nabla X),x)

then [y,x] in nabla X by A1, ZFMISC_1:87;

hence y in Class ((nabla X),x) by Th19; :: thesis: verum

( y in X iff y in Class ((nabla X),x) ) ;

hence Class ((nabla X),x) = X by TARSKI:2; :: thesis: verum