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