let H be ZF-formula; :: thesis: 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 ; :: thesis: ( a in variables_in H implies ( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 ) )
assume a in variables_in H ; :: thesis: ( 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; :: thesis: verum