theorem Th176: :: ZF_LANG1:176

for H being ZF-formula
for x, y being Variable st H is biconditional holds
H / (x,y) is biconditional