let A, x, y be set ; :: thesis: ( not x in A implies (x .--> y) | A = {} )
assume not x in A ; :: thesis: (x .--> y) | A = {}
then {x} misses A by ZFMISC_1:56;
then dom (x .--> y) misses A by Th19;
hence (x .--> y) | A = {} by RELAT_1:95; :: thesis: verum