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;

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;

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;

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

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 :: thesis: for a being object st a in {y,z} holds

not a in Free H

then
{y,z} misses Free H
by XBOOLE_0:3;not a in Free H

let a be object ; :: 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;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

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;

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;

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