The Modal Tree Widget
Modal Predicate Logics
[Click, or touch, on a formula to toggle selection on on and off. Select one item to extend the Tree, select two to close a branch. [Select two for extending with identity, necessityR etc,]]
Rod Girle  Modal Logics and Philosophy Chapter 4
will be a help here.
Modal Predicate S5
a) ∴(∀x)□Fx ⊃ □(∀x)Fx
b) ∴(∃x)□Fx ⊃ □(∃x)Fx
Modal Predicate Logic with Contingent Identity (S5QT=)
When there is identity in a tree, branches can be closed in either of two ways: the familiar way of selecting two formulas that contradict each other in the same world, or selecting a single formula like ~(a=a) which says that something is not identical to itself.
When substituting with identity in a tree you need to select two formulas: one is an identity, the other is any formula.
a) ∴ a=b ⊃ □a=b (hint, this is invalid in S5QT= ie you won't be able to close the tree)
b) ∴ a=b ⊃ (□Fa⊃□Fb)
c) ∴ □a=b ⊃ (Fa⊃Fb)
These are famous formulas in modal predicate logic
a) ∴ ◊(∃x)Fx⊃(∃x)◊Fx Barcan
b) ∴ (∃x)◊Fx⊃◊(∃x)Fx Barcan converse
c) ∴ (∀x)□Fx⊃□(∀x)Fx Barcan
d) ∴ □(∀x)Fx⊃(∀x)□Fx Barcan converse