let x, y, z be Variable; :: thesis: for H being ZF-formula
for E being non empty set
for f being Function of VAR ,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All x,y,z,H
let H be ZF-formula; :: thesis: for E being non empty set
for f being Function of VAR ,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All x,y,z,H
let E be non empty set ; :: thesis: for f being Function of VAR ,E st {x,y,z} misses Free H & E,f |= H holds
E,f |= All x,y,z,H
let f be Function of VAR ,E; :: thesis: ( {x,y,z} misses Free H & E,f |= H implies E,f |= All x,y,z,H )
assume that
A1: {x,y,z} misses Free H and
A2: E,f |= H ; :: thesis: E,f |= All x,y,z,H
A3: bound_in (All y,(All z,H)) = y by Lm2;

now

let a be set ; :: thesis: ( a in {y,z} implies not a in Free H )
assume a in {y,z} ; :: thesis: not a in Free H
then ( a = y or a = z ) by TARSKI:def 2;
then a in {x,y,z} by ENUMSET1:def 1;
hence not a in Free H by A1, XBOOLE_0:3; :: thesis: verum

end;

then {y,z} misses Free H by XBOOLE_0:3;
then A4: E,f |= All y,z,H by A2, Th11;
A5: ( All z,H is universal & the_scope_of (All z,H) = H ) by Lm2, ZF_LANG:16;
x in {x,y,z} by ENUMSET1:def 1;
then not x in Free H by A1, XBOOLE_0:3;
then not x in (Free H) \ {z} by XBOOLE_0:def 5;
then A6: not x in ((Free H) \ {z}) \ {y} by XBOOLE_0:def 5;
A7: bound_in (All z,H) = z by Lm2;
( All y,(All z,H) is universal & the_scope_of (All y,(All z,H)) = All z,H ) by Lm2, ZF_LANG:16;
then Free (All y,z,H) = (Free (All z,H)) \ {y} by A3, ZF_MODEL:1
.= ((Free H) \ {z}) \ {y} by A5, A7, ZF_MODEL:1 ;
hence E,f |= All x,y,z,H by A4, A6, Th10; :: thesis: verum