let A, B be set ; :: thesis: for x being object st not x in B holds
(A --> x) " B = {}
let x be object ; :: thesis: ( not x in B implies (A --> x) " B = {} )
assume A1: not x in B ; :: thesis: (A --> x) " B = {}
rng (A --> x) c= {x} by Th13;
then rng (A --> x) misses B by A1, XBOOLE_1:63, ZFMISC_1:50;
hence (A --> x) " B = {} by RELAT_1:138; :: thesis: verum