let x be Variable; :: thesis: for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
let H be ZF-formula; :: thesis: for E being non empty set
for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
let E be non empty set ; :: thesis: for f being Function of VAR,E st not x in Free H & E,f |= H holds
E,f |= All (x,H)
let f be Function of VAR,E; :: thesis: ( not x in Free H & E,f |= H implies E,f |= All (x,H) )
A1: len H = len H ;
for n being Nat holds S₁[n] from NAT_1:sch 4(Lm1);
hence ( not x in Free H & E,f |= H implies E,f |= All (x,H) ) by A1; :: thesis: verum