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