let X, Y be set ; :: thesis: ( ( for a being set holds
( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in Y iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ) implies X = Y )
assume that
A3: for a being set holds
( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) and
A4: for a being set holds
( a in Y iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) ; :: thesis: X = Y

now :: thesis: for a being object holds
( ( a in X implies a in Y ) & ( a in Y implies a in X ) )

let a be object ; :: thesis: ( ( a in X implies a in Y ) & ( a in Y implies a in X ) )
thus ( a in X implies a in Y ) :: thesis: ( a in Y implies a in X )

proof

assume a in X ; :: thesis: a in Y
then ex F being ZF-formula st
( F = a & F is_subformula_of H ) by A3;
hence a in Y by A4; :: thesis: verum

end;

assume a in Y ; :: thesis: a in X
then ex F being ZF-formula st
( F = a & F is_subformula_of H ) by A4;
hence a in X by A3; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum