defpred S₁[ set , set ] means ( $1 = $2 & P₁[$2] );
A1: for x, y, z being set st S₁[x,y] & S₁[x,z] holds
y = z ;
consider X being set such that
A2: for x being set holds
( x in X iff ex y being set st
( y in F₁() & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take X ; :: thesis: for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) )
let x be set ; :: thesis: ( x in X iff ( x in F₁() & P₁[x] ) )
( x in X iff ex y being set st
( y in F₁() & y = x & P₁[x] ) ) by A2;
hence ( x in X iff ( x in F₁() & P₁[x] ) ) ; :: thesis: verum