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