theorem :: ZF_LANG1:171

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