now

let x be set ; :: thesis: ( x in dom {} iff x in {} )

now

assume x in dom {} ; :: thesis: contradiction
then ex y being set st [x,y] in {} by Def4;
hence contradiction ; :: thesis: verum

end;

hence ( x in dom {} iff x in {} ) ; :: thesis: verum

end;

hence dom {} = {} by TARSKI:2; :: thesis: rng {} = {}

now

let y be set ; :: thesis: ( y in rng {} iff y in {} )

now

assume y in rng {} ; :: thesis: contradiction
then ex x being set st [x,y] in {} by Def5;
hence contradiction ; :: thesis: verum

end;

hence ( y in rng {} iff y in {} ) ; :: thesis: verum

end;

hence rng {} = {} by TARSKI:2; :: thesis: verum