let x be Variable; :: thesis: for F, H being ZF-formula holds
( F is_immediate_constituent_of All x,H iff F = H )
let F, H be ZF-formula; :: thesis: ( F is_immediate_constituent_of All x,H iff F = H )
thus ( F is_immediate_constituent_of All x,H implies F = H ) :: thesis: ( F = H implies F is_immediate_constituent_of All x,H )

proof

assume A1: F is_immediate_constituent_of All x,H ; :: thesis: F = H

A2: now

assume A3: All x,H = 'not' F ; :: thesis: contradiction
( (All x,H) . 1 = 4 & ('not' F) . 1 = 2 ) by Th34, FINSEQ_1:58;
hence contradiction by A3; :: thesis: verum

end;

now

given G being ZF-formula such that A4: ( All x,H = F '&' G or All x,H = G '&' F ) ; :: thesis: contradiction
( (F '&' G) . 1 = 3 & (G '&' F) . 1 = 3 & (All x,H) . 1 = 4 ) by Th33, Th34;
hence contradiction by A4; :: thesis: verum

end;

then ex y being Variable st All x,H = All y,F by A1, A2, Def39;
hence F = H by Th12; :: thesis: verum

end;

thus ( F = H implies F is_immediate_constituent_of All x,H ) by Def39; :: thesis: verum