let V be Universe; :: thesis: for X being Subclass of V
for E being non empty set
for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds
Diagram (H,E) in X
let X be Subclass of V; :: thesis: for E being non empty set
for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds
Diagram (H,E) in X
let E be non empty set ; :: thesis: for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds
Diagram (H,E) in X
let H be ZF-formula; :: thesis: ( X is closed_wrt_A1-A7 & E in X implies Diagram (H,E) in X )
defpred S₁[ ZF-formula] means Diagram ($1,E) in X;
assume A1: ( X is closed_wrt_A1-A7 & E in X ) ; :: thesis: Diagram (H,E) in X
then A2: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H] by Th19;
A3: for H being ZF-formula
for v1 being Element of VAR st S₁[H] holds
S₁[ All (v1,H)] by A1, Th21;
A4: for H, H9 being ZF-formula st S₁[H] & S₁[H9] holds
S₁[H '&' H9] by A1, Th20;
A5: for v1, v2 being Element of VAR holds
( S₁[v1 '=' v2] & S₁[v1 'in' v2] ) by A1, Th18;
for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A5, A2, A4, A3);
hence Diagram (H,E) in X ; :: thesis: verum