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 A5: 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 A6: x in X ; :: thesis: ( x in dom f & f . x = a )
hence x in dom f by A5, FUNCT_1:def 7; :: thesis: f . x = a
f . x in {a} by A5, A6, FUNCT_1:def 7;
hence f . x = a by TARSKI:def 1; :: thesis: verum

end;

assume A7: 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 A5, A7, FUNCT_1:def 7; :: thesis: verum

end;

assume A8: 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 object holds
( x in X iff ( x in dom f & f . x in {a} ) )

proof

let x be object ; :: 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 A9: x in X ; :: thesis: ( x in dom f & f . x in {a} )
hence x in dom f by A8; :: thesis: f . x in {a}
f . x = a by A8, A9;
hence f . x in {a} by TARSKI:def 1; :: thesis: verum

end;

assume A10: 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 A8, A10; :: thesis: verum

end;

hence X = eq_dom (f,a) by FUNCT_1:def 7; :: thesis: verum