let V be Universe; 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; 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 ; 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; ( X is closed_wrt_A1-A7 & E in X implies Diagram (H,E) in X )
defpred S1[ ZF-formula] means Diagram ($1,E) in X;
assume A1:
( X is closed_wrt_A1-A7 & E in X )
; Diagram (H,E) in X
then A2:
for H being ZF-formula st S1[H] holds
S1[ 'not' H]
by Th19;
A3:
for H being ZF-formula
for v1 being Element of VAR st S1[H] holds
S1[ All (v1,H)]
by A1, Th21;
A4:
for H, H9 being ZF-formula st S1[H] & S1[H9] holds
S1[H '&' H9]
by A1, Th20;
A5:
for v1, v2 being Element of VAR holds
( S1[v1 '=' v2] & S1[v1 'in' v2] )
by A1, Th18;
for H being ZF-formula holds S1[H]
from ZF_LANG1:sch 1(A5, A2, A4, A3);
hence
Diagram (H,E) in X
; verum