let A, B, C, x be set ; :: thesis: ( C c= A & not x in A implies ((id A) +* (B --> x)) " (C \ {x}) = C \ B )
assume that
A1: C c= A and
A2: not x in A ; :: thesis: ((id A) +* (B --> x)) " (C \ {x}) = C \ B
not x in C \ B

proof

assume x in C \ B ; :: thesis: contradiction
then x in C ;
hence contradiction by A1, A2; :: thesis: verum

end;

then C \ B misses {x} by ZFMISC_1:50;
then (C \ B) \ {x} = C \ B by XBOOLE_1:83;
hence ((id A) +* (B --> x)) " (C \ {x}) = C \ B by A1, Th17; :: thesis: verum