let E be non empty set ; :: thesis: for f being Function of VAR ,E
for H, H9 being ZF-formula holds
( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) )
let f be Function of VAR ,E; :: thesis: for H, H9 being ZF-formula holds
( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) )
let H, H9 be ZF-formula; :: thesis: ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) )
A1: ( E,f |= H iff f in St H,E ) by Def4;
A2: ( E,f |= H9 iff f in St H9,E ) by Def4;
( E,f |= H '&' H9 iff f in St (H '&' H9),E ) by Def4;
hence ( E,f |= H '&' H9 iff ( E,f |= H & E,f |= H9 ) ) by A1, A2, Th5; :: thesis: verum