I agree with your concern : the exercise is proposed before the explanation of the inference rules for the quantifiers : thus, we are not requested to use them.
The exercise asks to prove that the biconditional : ∀x Tet(b) ↔ ∃w Tet(b) is a logical truth, i.e. that
the two sides of the biconditional are logically equivalent (2nd ed : 2011, page 286).
The definition of logical equivalence is :
We say that two wffs with free variables are logically equivalent if, in
any possible circumstance, they are satified by the same objects. (page 278).
Note : if we want, we may consider only the non-trivial case :
∃w Tet(b) → ∀x Tet(b),
because for the other conditional, we have to note that : ∀x φ(x) → ∃w φ(x) holds in general.
The discussion about null quantication (page 283) has showed that :
if the variable x is not free in wff P, then we have the following
(logical) equivalences: ∀x P ⇔ P ⇔ ∃w P (see page 82 for the symbol : ⇔ which stay for logically equivalent, and is not the biconditional).
This means that : ∃w Tet(b), ∀x Tet(b) and Tet(b) are either all true or all false.
Consider the two cases :
(i) Tet(b) is t : then both ∃w Tet(b) and ∀x Tet(b) are t, and thus the biconditional : ∃w Tet(b) ↔ ∀x Tet(b) is t (because : t ↔ t is t);
(ii) Tet(b) is f : then both ∃w Tet(b) and ∀x Tet(b) are f, and thus the biconditional : ∃w Tet(b) ↔ ∀x Tet(b) is again t (because : f ↔ f is t).
Conclusion : in any possible circumstance, the formula ∃w Tet(b) ↔ ∀x Tet(b) is satisfied, and thus it is a logical truth.
For a derivation with the inference rules of the book (i.e. with Natural Deduction) we consider only the non-trivial case :
∃w Tet(b) → ∀x Tet(b).
Here we need to note that the (meta-) expressions φ(x,y) neither means that the listed variables occur free nor that no other ones occur free.
We have to "read carefully" the Universal Introduction (∀ Intro) rule (page 352) :
if we have a derivation of φ[c/x] (i.e. the formula obtained from φ(x) replacing all occurrences of the variable x with the term c) and c does not occur in φ or in any undischarged assumption of the derivation, then we are licensed to derive ∀xφ. In symbols : φ[c/x] ⊢ ∀x φ.
1) ∃w Tet(b) --- assumption [a]
start a subproof :
2) Tet(b) --- assumed for ∃ Elim (page 357) : we introduce a new constant symbol, say c, replacing all the occurrences of w in Tet(b) with c, along with the assumption that the object denoted by c satisfies the formula Tet(b); but there is no occurrences of w in Tet(b), thus the result of Tet(b)[c/w] is Tet(b) itself.
3) ∀x Tet(b) --- from 2) by ∀ Intro
end of subproof;
4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ Elim
5) ∃w Tet(b) → ∀x Tet(b) --- from 1) and 4) by → Intro, discharging the assumption [a].