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, ZF_LANG:16;
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