A5: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds
P1[H]
proof
let H be ZF-formula; :: thesis: ( H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] implies P1[H] )
assume H is conjunctive ; :: thesis: ( not P1[ the_left_argument_of H] or not P1[ the_right_argument_of H] or P1[H] )
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
hence ( not P1[ the_left_argument_of H] or not P1[ the_right_argument_of H] or P1[H] ) by A3; :: thesis: verum
end;
A6: for H being ZF-formula st H is atomic holds
P1[H]
proof
let H be ZF-formula; :: thesis: ( H is atomic implies P1[H] )
assume A7: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: P1[H]
A8: ( H is being_membership implies P1[H] ) by A1;
( H is being_equality implies P1[H] ) by A1;
hence P1[H] by A7, A8; :: thesis: verum
end;
A9: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds
P1[H]
proof
let H be ZF-formula; :: thesis: ( H is universal & P1[ the_scope_of H] implies P1[H] )
assume H is universal ; :: thesis: ( not P1[ the_scope_of H] or P1[H] )
then H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
hence ( not P1[ the_scope_of H] or P1[H] ) by A4; :: thesis: verum
end;
A10: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds
P1[H]
proof
let H be ZF-formula; :: thesis: ( H is negative & P1[ the_argument_of H] implies P1[H] )
assume H is negative ; :: thesis: ( not P1[ the_argument_of H] or P1[H] )
then H = 'not' (the_argument_of H) by ZF_LANG:def 30;
hence ( not P1[ the_argument_of H] or P1[H] ) by A2; :: thesis: verum
end;
thus for H being ZF-formula holds P1[H] from ZF_LANG:sch 1(A6, A10, A5, A9); :: thesis: verum