:: Families of Subsets
:: by Andrzej Trybulec
::
:: Received December 13, 2012
:: 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;