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] )