x 'in' y is ZF-formula-like

proof

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

end;

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