I'm tryng to demonstrate with fitch notation this:
{∀x (A(x) ↔ B(x)), ∀x (A(x))} |= ∀x (B(x))
Here what I tried: https://i.stack.imgur.com/7S5Zy.png
Someone can explain me how i can obtain ∀x (B(x)? Because with the introduction rule of ∀x I can obtain only ∀x (A(x) -> B(x))
In the version of a Fitch style proof that you are apparently using, when you get to your line 5, you can go on to just quantify by UQ int.
Thus
$1\quad \forall x(Ax \to Bx)\\ 2\quad \forall xAx\\ 3\quad\quad d\mid \quad Ad \to Bd\\ 4\quad\quad \ \mid \quad Ad\\ 5\quad\quad \ \mid \quad Bd\\ 6\quad \forall xBx$
Check out your version of the universal quantifier introduction rule which we are appealing to at the last step!
[Actually I don't think this is the most transparent version of the Fitch style proof-layout, although it is [near] Thomason's for example. I prefer to only indent columns when a new, independent, temporary assumption is being made which doesn't follow from what's gone before, e.g. as when starting a conditional proof, or making an assumption for reductio. So even in a Fitch-style natural deduction system where you indent to the right everytime you make a new assumption, and track back to the left when you eventually discharge that assumption, I'd prefer to write this proof simply as
$1\quad \forall x(Ax \to Bx)\\ 2\quad \forall xAx\\ 3\quad\ Ad \to Bd\\ 4\quad Ad\\ 5\quad Bd\\ 6\quad \forall xBx$
Since, whatever $d$ picks out, (3) and (4) follow from (1) and (2) without further ado. And (6) follows from (5) as (5) depends on no special premisses about $d$.]