theorem :: FUNCT_1:21

for Y being set
for x being object
for f being Function holds
( x in dom ((id Y) * f) iff ( x in dom f & f . x in Y ) )