x '=' y is Element of WFF by Def8;
hence x '=' y is ZF-formula-like by Def9; :: thesis: verum