for H being ZF-formula holds P₁[H]

A1: for x1, x2 being Variable holds
( P₁[x1 '=' x2] & P₁[x1 'in' x2] ) and
A2: for H being ZF-formula st P₁[H] holds
P₁[ 'not' H] and
A3: for H1, H2 being ZF-formula st P₁[H1] & P₁[H2] holds
P₁[H1 '&' H2] and
A4: for H being ZF-formula
for x being Variable st P₁[H] holds
P₁[ All (x,H)]