I know that in propositional logic we have the truth tables to verify the equivalence between two statements, but in first-order logic i understand that they are not used, then, what method is used to verify an equivalence?.
The equivalence "$\forall x (P(x)\land Q(x)) \iff \forall x P(x) \land \forall x Q(x)$" intuitively makes sense to me, as well as the equivalence "$\exists x (P(x) \land \forall y [P(y) \implies x=y]) \iff \exists x P(x) \land \forall y \forall z (P(y) \land P(z) \implies y=z)$", but "intuitively" no is useful to me, as a formal language it must has an algoritm or method that allow me to know if an equivalence is true or false in a formal way, like the propositional logic.
I think the key is perhaps in the interpretation of each variable involved in the statements and their universe of discourse, but it seems somewhat informal to me.
You may be surprised to learn that there does not exist an algorithm that can always decide whether a first-order logic equivalence holds or not! This is known as the undecidability of first-order logic. It was Alan Turing who showed this based on his work on Turing-machines.
That said, there are a number of methods that can decide equivalence vs non=-equivalence for some (well, a lot, just not all!) pairs of statements. So for some pairs of statements, such a method will be able to determine that they are equivalent, for other pairs it will be able to determine that they are not equivalent, but for some pairs, the algorithm will run forever and never provide an answer either way. (again, it was Turing who showed the connection between the undecidability of the halting problem and the undecidability of first-order logic).
One popular such method is truth trees, also known as semantic tableaux. It takes too much time to lay out exactly how that method works in a forum like this, but there should be plenty of material online discussing how exactly that method works. If you carefully create an algorithm based on this method, then for any pair of equivalent statements it will be able to eventually determine that they are equivalent, but for some pairs of non-equivalent statements it will run forever.... but of course you don't always know that it will run forever (maybe it stops 10 seconds from now!), and so you don't know that you are dealing with a non-equivalent pair.
Modern automated theorem provers (checkers, really) are often based on another method, called resolution. That method is a bit friendlier for machines, but less friendly for humans. Again, search for it online if you want to know more.