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

F₁() = F₂()

provided

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