defpred S₁[ set ] means ex F being ZF-formula st
( F = $1 & F is_subformula_of H );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in NAT * & S₁[a] ) ) from XFAMILY:sch 1();
take X ; :: thesis: for a being set holds
( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) )
let a be set ; :: thesis: ( a in X iff ex F being ZF-formula st
( F = a & F is_subformula_of H ) )
thus ( a in X implies ex F being ZF-formula st
( F = a & F is_subformula_of H ) ) by A1; :: thesis: ( ex F being ZF-formula st
( F = a & F is_subformula_of H ) implies a in X )
given F being ZF-formula such that A2: ( F = a & F is_subformula_of H ) ; :: thesis: a in X
F in NAT * by FINSEQ_1:def 11;
hence a in X by A1, A2; :: thesis: verum