let X1 be non empty set ; :: thesis: ( ( for x1 being Element of X1 holds
( P1[x1] iff P2[x1] ) ) implies { y1 where y1 is Element of X1 : P1[y1] } = { z1 where z1 is Element of X1 : P2[z1] } )
assume A1: for x1 being Element of X1 holds
( P1[x1] iff P2[x1] ) ; :: thesis: { y1 where y1 is Element of X1 : P1[y1] } = { z1 where z1 is Element of X1 : P2[z1] }
for X1 being non empty set st ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) holds
{ y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } from DOMAIN_1:sch 5();
 hence { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } by A1; :: according to XBOOLE_0:def 10 :: thesis: { z1 where z1 is Element of X1 : P2[z1] } c= { y1 where y1 is Element of X1 : P1[y1] }
for X1 being non empty set st ( for x1 being Element of X1 st P2[x1] holds
P1[x1] ) holds
{ y1 where y1 is Element of X1 : P2[y1] } c= { z1 where z1 is Element of X1 : P1[z1] } from DOMAIN_1:sch 5();
 hence { z1 where z1 is Element of X1 : P2[z1] } c= { y1 where y1 is Element of X1 : P1[y1] } by A1; :: thesis: verum