let A be Subset of [:NAT,NAT:]; :: thesis: proj1 A = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A }
set A1 = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ;
A1: proj1 A c= { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 A or x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } )
assume x in proj1 A ; :: thesis: x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A }
then consider y being object such that
A2: [x,y] in A by XTUPLE_0:def 12;
ex x1, y1 being object st
( x1 in NAT & y1 in NAT & [x,y] = [x1,y1] ) by A2, ZFMISC_1:def 2;
then reconsider x = x, y = y as Element of NAT by XTUPLE_0:1;
( [x,y] in A & y is Element of NAT ) by A2;
hence x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ; :: thesis: verum

end;

{ x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } c= proj1 A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } or x in proj1 A )
assume x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ; :: thesis: x in proj1 A
then ex x1 being Element of NAT st
( x = x1 & ex y being Element of NAT st [x1,y] in A ) ;
hence x in proj1 A by XTUPLE_0:def 12; :: thesis: verum

end;

hence proj1 A = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by A1; :: thesis: verum