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 A1: ( C c= A & 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; :: thesis: verum

end;

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