Consider the following premises. forall z: W(z) <-> W_2(z). W_2(i) -> r. r -> W(i). Can we infer r <-> W(i) from them? If possible, name the inference rules being used at each step.
 From forall z: W(z) <-> W_2(z) we can infer W(i) <-> W_2(i) via universal instantiation. From W(i) <-> W_2(i) we can infer W(i) -> W_2(i) via biconditional elimination. From W(i) -> W_2(i), W_2(i) -> r we can infer W(i) -> r via transitivity. Finally, from r -> W(i), W(i) -> r we can infer r <-> W(i) via biconditional introduction. Therefore, the answer is yes.