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