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