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 A1: ( {x,y,z} misses Free H & E,f |= H ) ; :: thesis: E,f |= All x,y,z,H

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 A2: E,f |= All y,z,H by A1, Th11;
A3: ( All y,z,H = All y,(All z,H) & All y,(All z,H) is universal & the_scope_of (All y,(All z,H)) = All z,H & bound_in (All y,(All z,H)) = y & All z,H is universal & the_scope_of (All z,H) = H & bound_in (All z,H) = z ) by Lm2, ZF_LANG:16;
then A4: Free (All y,z,H) = (Free (All z,H)) \ {y} by ZF_MODEL:1
.= ((Free H) \ {z}) \ {y} by A3, ZF_MODEL:1 ;
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 not x in ((Free H) \ {z}) \ {y} by XBOOLE_0:def 5;
hence E,f |= All x,y,z,H by A2, A4, Th10; :: thesis: verum