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 iff 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 iff E,f |= H9 ) )
let H, H9 be ZF-formula; :: thesis: ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) )
( E,f |= (H => H9) '&' (H9 => H) iff ( E,f |= H => H9 & E,f |= H9 => H ) ) by Th15;
hence ( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) ) by Th18; :: thesis: verum