let s be QC-formula; :: thesis: for y, x being bound_QC-variable holds
( y in still_not-bound_in (Ex (x,s)) iff ( y in still_not-bound_in s & y <> x ) )
let y, x be bound_QC-variable; :: 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