uniqueness
for b1, b2 being set st ( for x being object holds ( x in b1 iff x = y ) ) & ( for x being object holds ( x in b2 iff x = y ) ) holds b1= b2
uniqueness
for b1, b2 being set st ( for x being object holds ( x in b1 iff ( x = y or x = z ) ) ) & ( for x being object holds ( x in b2 iff ( x = y or x = z ) ) ) holds b1= b2
commutativity
for b1 being set for y, z being object st ( for x being object holds ( x in b1 iff ( x = y or x = z ) ) ) holds for x being object holds ( x in b1 iff ( x = z or x = y ) )
;
:: deftheorem Def2 defines {TARSKI:def 2 : for y, z being object for b3 being set holds ( b3={y,z} iff for x being object holds ( x in b3 iff ( x = y or x = z ) ) );
uniqueness
for b1, b2 being set st ( for x being object holds ( x in b1 iff ex Y being set st ( x in Y & Y in X ) ) ) & ( for x being object holds ( x in b2 iff ex Y being set st ( x in Y & Y in X ) ) ) holds b1= b2
for x being object for X being set st x in X holds ex Y being set st ( Y in X & ( for x being object holds ( not x in X or not x in Y ) ) ) byTARSKI_0:5;
definition
let x, X be set ; :: original: in redefine predx in X; asymmetry
for x, X being set st R2(b1,b2) holds not R2(b2,b1)