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

scheme :: XFAMILY:sch 1
Separation{ F₁() -> set , P₁[ object ] } :

ex X being set st
for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) )

proof end;

scheme :: XFAMILY:sch 2
Extensionality{ F₁() -> set , F₂() -> set , P₁[ set ] } :

F₁() = F₂()

provided

A1: for x being set holds
( x in F₁() iff P₁[x] ) and
A2: for x being set holds
( x in F₂() iff P₁[x] )

proof end;

scheme :: XFAMILY:sch 3
SetEq{ P₁[ set ] } :

for X1, X2 being set st ( for x being set holds
( x in X1 iff P₁[x] ) ) & ( for x being set holds
( x in X2 iff P₁[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;