let A, x, B be set ; :: thesis: ( not x in B implies (A --> x) " B = {} )
A1: rng (A --> x) c= {x} by Th19;
assume not x in B ; :: thesis: (A --> x) " B = {}
then rng (A --> x) misses B by A1, XBOOLE_1:63, ZFMISC_1:56;
hence (A --> x) " B = {} by RELAT_1:173; :: thesis: verum