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
A1: now :: thesis: for G being ZF-formula holds
( not All (x,H) = F '&' G & not All (x,H) = G '&' F )
given G being ZF-formula such that A2: ( All (x,H) = F '&' G or All (x,H) = G '&' F ) ; :: thesis: contradiction
( (F '&' G) . 1 = 3 & (G '&' F) . 1 = 3 ) by Th16;
hence contradiction by A2, Th17; :: thesis: verum
end;
A3: now :: thesis: not All (x,H) = 'not' F
assume A4: All (x,H) = 'not' F ; :: thesis: contradiction
(All (x,H)) . 1 = 4 by Th17;
hence contradiction by A4, FINSEQ_1:41; :: thesis: verum
end;
assume F is_immediate_constituent_of All (x,H) ; :: thesis: F = H
then ex y being Variable st All (x,H) = All (y,F) by A3, A1;
hence F = H by Th3; :: thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of All (x,H) ) ; :: thesis: verum