let H be ZF-formula; for a being set st a in variables_in H holds
( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )
let a be set ; ( a in variables_in H implies ( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 ) )
assume
a in variables_in H
; ( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )
then
not a in {0,1,2,3,4}
by XBOOLE_0:def 5;
then
not a in {0,1} \/ {2,3,4}
by ENUMSET1:8;
then
( not a in {0,1} & not a in {2,3,4} )
by XBOOLE_0:def 3;
hence
( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )
by ENUMSET1:def 1, TARSKI:def 2; verum