let x, y be set ; :: thesis: for R being Relation st R = {[x,y]} holds
( dom R = {x} & rng R = {y} )
let R be Relation; :: thesis: ( R = {[x,y]} implies ( dom R = {x} & rng R = {y} ) )
assume A1: R = {[x,y]} ; :: thesis: ( dom R = {x} & rng R = {y} )
for z being set holds
( z in dom R iff z in {x} )

proof

let z be set ; :: thesis: ( z in dom R iff z in {x} )
thus ( z in dom R implies z in {x} ) :: thesis: ( z in {x} implies z in dom R )

proof

assume z in dom R ; :: thesis: z in {x}
then consider b being set such that
A2: [z,b] in R by Def4;
[z,b] = [x,y] by A1, A2, TARSKI:def 1;
then z = x by ZFMISC_1:27;
hence z in {x} by TARSKI:def 1; :: thesis: verum

end;

assume z in {x} ; :: thesis: z in dom R
then z = x by TARSKI:def 1;
then [z,y] in R by A1, TARSKI:def 1;
hence z in dom R by Def4; :: thesis: verum

end;

hence dom R = {x} by TARSKI:1; :: thesis: rng R = {y}
for z being set holds
( z in rng R iff z in {y} )

proof

let z be set ; :: thesis: ( z in rng R iff z in {y} )
thus ( z in rng R implies z in {y} ) :: thesis: ( z in {y} implies z in rng R )

proof

assume z in rng R ; :: thesis: z in {y}
then consider a being set such that
A3: [a,z] in R by Def5;
[a,z] = [x,y] by A1, A3, TARSKI:def 1;
then z = y by ZFMISC_1:27;
hence z in {y} by TARSKI:def 1; :: thesis: verum

end;

assume z in {y} ; :: thesis: z in rng R
then z = y by TARSKI:def 1;
then [x,z] in R by A1, TARSKI:def 1;
hence z in rng R by Def5; :: thesis: verum

end;

hence rng R = {y} by TARSKI:1; :: thesis: verum