let X be set ; :: thesis: ( X = eq_dom f,a iff for x being set holds
( x in X iff ( x in dom f & f . x = a ) ) )
thus ( X = eq_dom f,a implies for x being set holds
( x in X iff ( x in dom f & f . x = a ) ) ) :: thesis: ( ( for x being set holds
( x in X iff ( x in dom f & f . x = a ) ) ) implies X = eq_dom f,a )

proof

assume Z: X = eq_dom f,a ; :: thesis: for x being set holds
( x in X iff ( x in dom f & f . x = a ) )
let x be set ; :: thesis: ( x in X iff ( x in dom f & f . x = a ) )
thus ( x in X implies ( x in dom f & f . x = a ) ) :: thesis: ( x in dom f & f . x = a implies x in X )

proof

assume Z1: x in X ; :: thesis: ( x in dom f & f . x = a )
hence x in dom f by Z, FUNCT_1:def 13; :: thesis: f . x = a
f . x in {a} by Z, Z1, FUNCT_1:def 13;
hence f . x = a by TARSKI:def 1; :: thesis: verum

end;

assume Z1: x in dom f ; :: thesis: ( not f . x = a or x in X )
assume f . x = a ; :: thesis: x in X
then f . x in {a} by TARSKI:def 1;
hence x in X by Z, Z1, FUNCT_1:def 13; :: thesis: verum

end;

assume Z: for x being set holds
( x in X iff ( x in dom f & f . x = a ) ) ; :: thesis: X = eq_dom f,a
for x being set holds
( x in X iff ( x in dom f & f . x in {a} ) )

proof

let x be set ; :: thesis: ( x in X iff ( x in dom f & f . x in {a} ) )
thus ( x in X implies ( x in dom f & f . x in {a} ) ) :: thesis: ( x in dom f & f . x in {a} implies x in X )

proof

assume Z1: x in X ; :: thesis: ( x in dom f & f . x in {a} )
hence x in dom f by Z; :: thesis: f . x in {a}
f . x = a by Z1, Z;
hence f . x in {a} by TARSKI:def 1; :: thesis: verum

end;

assume Z1: x in dom f ; :: thesis: ( not f . x in {a} or x in X )
assume f . x in {a} ; :: thesis: x in X
then f . x = a by TARSKI:def 1;
hence x in X by Z, Z1; :: thesis: verum

end;

hence X = eq_dom f,a by FUNCT_1:def 13; :: thesis: verum