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_{1}[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

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

hence ( not x in Free H & E,f |= H implies E,f |= All (x,H) ) by A1; :: thesis: verum