let A be QC-alphabet ; :: thesis: for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let s be QC-formula of A; :: thesis: for x, y being bound_QC-variable of A holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let x, y be bound_QC-variable of A; :: thesis: ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
still_not-bound_in (Ex (x,s)) = (still_not-bound_in s) \ {x} by QC_LANG3:19;
hence ( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) ) by ZFMISC_1:56; :: thesis: verum