let x, y be Variable; :: thesis: Subformulae (x '=' y) = {(x '=' y)}

now

let a be set ; :: thesis: ( ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) & ( a in {(x '=' y)} implies a in Subformulae (x '=' y) ) )
thus ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) :: thesis: ( a in {(x '=' y)} implies a in Subformulae (x '=' y) )

proof

assume a in Subformulae (x '=' y) ; :: thesis: a in {(x '=' y)}
then consider F being ZF-formula such that
A1: ( F = a & F is_subformula_of x '=' y ) by Def42;
F = x '=' y by A1, Th97;
hence a in {(x '=' y)} by A1, TARSKI:def 1; :: thesis: verum

end;

assume a in {(x '=' y)} ; :: thesis: a in Subformulae (x '=' y)
then ( a = x '=' y & x '=' y is_subformula_of x '=' y ) by Th79, TARSKI:def 1;
hence a in Subformulae (x '=' y) by Def42; :: thesis: verum

end;

hence Subformulae (x '=' y) = {(x '=' y)} by TARSKI:2; :: thesis: verum