let H be ZF-formula; :: thesis: for x, y being Variable holds
( H is being_membership iff H / (x,y) is being_membership )
let x, y be Variable; :: thesis: ( H is being_membership iff H / (x,y) is being_membership )
thus ( H is being_membership implies H / (x,y) is being_membership ) :: thesis: ( H / (x,y) is being_membership implies H is being_membership )

proof

given x1, x2 being Variable such that A1: H = x1 'in' x2 ; :: according to ZF_LANG:def 11 :: thesis: H / (x,y) is being_membership
ex z1, z2 being Variable st H / (x,y) = z1 'in' z2 by A1, Th169;
hence H / (x,y) is being_membership by ZF_LANG:5; :: thesis: verum

end;

assume H / (x,y) is being_membership ; :: thesis: H is being_membership
then A2: (H / (x,y)) . 1 = 1 by ZF_LANG:19;
3 <= len H by ZF_LANG:13;
then 1 <= len H by XXREAL_0:2;
then A3: 1 in dom H by FINSEQ_3:25;
y <> 1 by Th148;
then H . 1 <> x by A2, A3, Def4;
then 1 = H . 1 by A2, A3, Def4;
hence H is being_membership by ZF_LANG:25; :: thesis: verum