x '=' y is ZF-formula-like

proof

thus x '=' y is Element of WFF by Def8; :: according to ZF_LANG:def 9 :: thesis: verum

end;

hence x '=' y is ZF-formula-like ; :: thesis: verum