defpred S₁[ set ] means ex j being set st
( j in J & j in dom A & $1 in A . j );
let A1, A2 be set ; :: thesis: ( ( for x being set holds
( x in A1 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) & ( for x being set holds
( x in A2 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ) implies A1 = A2 )
assume that
A5: for x being set holds
( x in A1 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) and
A6: for x being set holds
( x in A2 iff ex j being set st
( j in J & j in dom A & x in A . j ) ) ; :: thesis: A1 = A2
A7: for x being set holds
( x in A2 iff S₁[x] ) by A6;
A8: for x being set holds
( x in A1 iff S₁[x] ) by A5;
A1 = A2 from XBOOLE_0:sch 2(A8, A7);
hence A1 = A2 ; :: thesis: verum