let X1 be non empty set ; :: thesis: ( ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) implies { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] } )
assume A1:
for x1 being Element of X1 st P1[x1] holds
P2[x1]
; :: thesis: { y1 where y1 is Element of X1 : P1[y1] } c= { z1 where z1 is Element of X1 : P2[z1] }
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { y1 where y1 is Element of X1 : P1[y1] } or a in { z1 where z1 is Element of X1 : P2[z1] } )
assume
a in { x1 where x1 is Element of X1 : P1[x1] }
; :: thesis: a in { z1 where z1 is Element of X1 : P2[z1] }
then consider x1 being Element of X1 such that
A2:
a = x1
and
A3:
P1[x1]
;
P2[x1]
by A1, A3;
hence
a in { z1 where z1 is Element of X1 : P2[z1] }
by A2; :: thesis: verum