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 v1, v2 being Element of VAR holds
( S₁[v1 '=' v2] & S₁[v1 'in' v2] ) by Th18;
A3: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H] by A1, Th19;
A4: for H, H' being ZF-formula st S₁[H] & S₁[H'] holds
S₁[H '&' H'] by A1, Th20;
A5: for H being ZF-formula
for v1 being Element of VAR st S₁[H] holds
S₁[ All v1,H] by A1, Th21;
for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A2, A3, A4, A5);
hence Diagram H,E in X ; :: thesis: verum