defpred S_{2}[ object ] means ( $1 in WFF & S_{1}[$1] );

let X1, X2 be set ; :: thesis: ( ( for e being object holds

( e in X1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being object holds

( e in X2 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) implies X1 = X2 )

assume that

A1: for e being object holds

( e in X1 iff S_{2}[e] )
and

A2: for e being object holds

( e in X2 iff S_{2}[e] )
; :: thesis: X1 = X2

thus X1 = X2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum

let X1, X2 be set ; :: thesis: ( ( for e being object holds

( e in X1 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being object holds

( e in X2 iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) implies X1 = X2 )

assume that

A1: for e being object holds

( e in X1 iff S

A2: for e being object holds

( e in X2 iff S

thus X1 = X2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum