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).
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 case (the other one is similar):
∃w Tet(b) → ∀x Tet(b).
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 φ.
We have to note that the (meta-) expressions φ(x,y) neither means that the listed variables occur free nor that no other ones occur free.
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].