Yes. Adding the usual axiom of (dependent) functional extensionality to Coq is believed to be sound whether Set is left predicative (the factory settings) or made impredicative with the flag -impredicative-set.

Why we are confident:

1. What the axiom says
   Functional extensionality is the sentence

   ∀ (A:Type) (B:A→Type) (f g : ∀x, B x),
        (∀x, f x = g x)  →  f = g .
   

(The usual non-dependent variant is the special case where B does not depend on x.)

2. A model in ordinary set theory
   A standard “proof-irrelevant” set–theoretic model of the Calculus of Constructions interprets
   • each Coq type as a ZFC set taken from some Grothendieck universe
   • the identity type x =_A y as the singleton set when x = y in ZFC and the empty set otherwise.

In this model
• Prop is interpreted by the two–element set {∅, {∅}},
• Set is interpreted by one chosen Grothendieck universe U₀,
and the higher Type_i by larger universes U_{i+1}.

The interpretation is exactly the same whether Set is taken to be predicative or impredicative inside Coq, because from the outside we still look at all sets in U₀.
Two functions are equal in ZFC iff they coincide on every argument, so the sentence that Coq calls functional extensionality is always true in the model. Therefore enriching Coq with that sentence cannot create new theorems about sets that were not already true: the axiom is consistent relative to ZFC.

3. Historical evidence
   • The original Calculus of Constructions (CoC) used a single impredicative universe ― essentially today’s Set. Werner (1994), Luo (1995) and others gave set-theoretic models for that system, and functional extensionality holds in all those models.
   • Launching today’s Coq with -impredicative-set and importing the library file Coq.Logic.FunctionalExtensionality merely declares the axiom; nothing special is required, and no inconsistency has ever been exhibited.

4. Things that do become delicate
   Impredicativity for Set interacts badly with strong elimination and with assuming proof irrelevance for every type in Set (Reynolds’ abstraction paradox). Functional extensionality alone does not imply those principles, so the paradoxes do not arise merely from adding it.

Bottom line

• Without extra axioms Coq cannot prove functional extensionality, whether Set is predicative or impredicative.
• Postulating the axiom is, however, compatible with both variants. The FAQ mentions only the predicative case because that is the default mode of Coq, not because the impredicative case would be problematic.