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:58;
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] )
proof
given x1, x2 being Variable such that A9: H = x1 'in' x2 ; :: according to ZF_LANG:def 11 :: thesis: P1[H]
thus P1[H] by A1, A9; :: thesis: verum
end;
( H is being_equality implies P1[H] )
proof
given x1, x2 being Variable such that A10: H = x1 '=' x2 ; :: according to ZF_LANG:def 10 :: thesis: P1[H]
thus P1[H] by A1, A10; :: thesis: verum
end;
hence P1[H] by A7, A8; :: thesis: verum
end;
A11: 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:62;
hence ( not P1[ the_scope_of H] or P1[H] ) by A4; :: thesis: verum
end;
A12: 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, A12, A5, A11); :: thesis: verum