set X = { F3(j) where j is Element of F1() : j in{F2()} } ;
for x being object holds ( x in F3(F2()) iff ex Y being set st ( x in Y & Y in { F3(j) where j is Element of F1() : j in{F2()} } ) )
let x be object ; :: thesis: ( x in F3(F2()) iff ex Y being set st ( x in Y & Y in { F3(j) where j is Element of F1() : j in{F2()} } ) ) thus
( x in F3(F2()) implies ex Y being set st ( x in Y & Y in { F3(j) where j is Element of F1() : j in{F2()} } ) )
:: thesis: ( ex Y being set st ( x in Y & Y in { F3(j) where j is Element of F1() : j in{F2()} } ) implies x in F3(F2()) )