theorem Th76: :: ZF_LANG:76

for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x '=' y iff H = x '=' y )