let x, y be Variable; :: thesis: for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

let H be ZF-formula; :: thesis: for E being non empty set

for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

let E be non empty set ; :: thesis: for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

let f be Function of VAR,E; :: thesis: ( {x,y} misses Free H & E,f |= H implies E,f |= All (x,y,H) )

assume that

A1: {x,y} misses Free H and

A2: E,f |= H ; :: thesis: E,f |= All (x,y,H)

A3: bound_in (All (y,H)) = y by Lm2;

( All (y,H) is universal & the_scope_of (All (y,H)) = H ) by Lm2;

then A4: Free (All (y,H)) = (Free H) \ {y} by A3, ZF_MODEL:1;

x in {x,y} by TARSKI:def 2;

then not x in Free H by A1, XBOOLE_0:3;

then A5: not x in Free (All (y,H)) by A4, XBOOLE_0:def 5;

y in {x,y} by TARSKI:def 2;

then not y in Free H by A1, XBOOLE_0:3;

then E,f |= All (y,H) by A2, Th10;

hence E,f |= All (x,y,H) by A5, Th10; :: thesis: verum

for E being non empty set

for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

let H be ZF-formula; :: thesis: for E being non empty set

for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

let E be non empty set ; :: thesis: for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

let f be Function of VAR,E; :: thesis: ( {x,y} misses Free H & E,f |= H implies E,f |= All (x,y,H) )

assume that

A1: {x,y} misses Free H and

A2: E,f |= H ; :: thesis: E,f |= All (x,y,H)

A3: bound_in (All (y,H)) = y by Lm2;

( All (y,H) is universal & the_scope_of (All (y,H)) = H ) by Lm2;

then A4: Free (All (y,H)) = (Free H) \ {y} by A3, ZF_MODEL:1;

x in {x,y} by TARSKI:def 2;

then not x in Free H by A1, XBOOLE_0:3;

then A5: not x in Free (All (y,H)) by A4, XBOOLE_0:def 5;

y in {x,y} by TARSKI:def 2;

then not y in Free H by A1, XBOOLE_0:3;

then E,f |= All (y,H) by A2, Th10;

hence E,f |= All (x,y,H) by A5, Th10; :: thesis: verum