theorem Th158: :: ZF_LANG1:158

for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 '&' G2 = (H1 '&' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )