let A, B, C, x be set ; ( 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
; ((id A) +* (B --> x)) " (C \ {x}) = C \ B
not x in C \ B
by A1, A2;
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, Th16; verum