defpred S₂[ object ] means ( $1 in WFF & S₁[$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₂[e] ) and
A2: for e being object holds
( e in X2 iff S₂[e] ) ; :: thesis: X1 = X2
thus X1 = X2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum