:: Families of Subsets
:: by Andrzej Trybulec
::
:: Copyright (c) 2012-2021 Association of Mizar Users

scheme :: XFAMILY:sch 1
Separation{ F1() -> set , P1[ object ] } :
ex X being set st
for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
proof end;

scheme :: XFAMILY:sch 2
Extensionality{ F1() -> set , F2() -> set , P1[ set ] } :
F1() = F2()
provided
A1: for x being set holds
( x in F1() iff P1[x] ) and
A2: for x being set holds
( x in F2() iff P1[x] )
proof end;

scheme :: XFAMILY:sch 3
SetEq{ P1[ set ] } :
for X1, X2 being set st ( for x being set holds
( x in X1 iff P1[x] ) ) & ( for x being set holds
( x in X2 iff P1[x] ) ) holds
X1 = X2
proof end;

definition
let x be object ;
:: original: 1
redefine func x 1 -> set ;
coherence
x 1 is set
by TARSKI:1;
:: original: 2
redefine func x 2 -> set ;
coherence
x 2 is set
by TARSKI:1;
end;

definition
let x be object ;
:: original: 1_3
redefine func x 1_3 -> set ;
coherence
x 1_3 is set
by TARSKI:1;
:: original: 2_3
redefine func x 2_3 -> set ;
coherence
x 2_3 is set
by TARSKI:1;
end;

definition
let x be object ;
:: original: 1_4
redefine func x 1_4 -> set ;
coherence
x 1_4 is set
by TARSKI:1;
:: original: 2_4
redefine func x 2_4 -> set ;
coherence
x 2_4 is set
by TARSKI:1;
end;