let x, y be Variable; :: thesis: for H being ZF-formula holds
( H is_subformula_of x '=' y iff H = x '=' y )
let H be ZF-formula; :: thesis: ( H is_subformula_of x '=' y iff H = x '=' y )
thus ( H is_subformula_of x '=' y implies H = x '=' y ) :: thesis: ( H = x '=' y implies H is_subformula_of x '=' y )

proof

assume A1: H is_subformula_of x '=' y ; :: thesis: H = x '=' y
assume H <> x '=' y ; :: thesis: contradiction
then H is_proper_subformula_of x '=' y by A1;
then ex F being ZF-formula st F is_immediate_constituent_of x '=' y by Th63;
hence contradiction by Th50; :: thesis: verum

end;

thus ( H = x '=' y implies H is_subformula_of x '=' y ) by Th59; :: thesis: verum