defpred S₁[ set ] means ex x being bound_QC-variable ex p being Element of CQC-WFF st $1 = Ex (x,p);
consider X being set such that
A1: for a being set holds
( a in X iff ( a in CQC-WFF & S₁[a] ) ) from XBOOLE_0:sch 1();
for a being set st a in X holds
a in CQC-WFF by A1;
then reconsider X = X as Subset of CQC-WFF by TARSKI:def 3;
take X ; :: thesis: for a being set holds
( a in X iff ex x being bound_QC-variable ex p being Element of CQC-WFF st a = Ex (x,p) )
thus for a being set holds
( a in X iff ex x being bound_QC-variable ex p being Element of CQC-WFF st a = Ex (x,p) ) by A1; :: thesis: verum