Is it a valid inference (in, say, any quantified modal logic S5 system) to go from ◊(∃x)◻Fx and ◻(∀x)(Fx --> E!x) to ◊(∃x)◻(Fx & E!x)? (E!x is the existence predicate, by the way.)
I am assuming, that there is a domain of objects that is common to all worlds, and the existence predicate E! signifies actualisation in each world (although that does not matter).
Your inference is valid. In S5 accessibility is an equivalence relation. From your first premise you get an object a which in all (here S5 was used) worlds lies in the extension of F. By your second premise, it also E!-exists in all worlds. Therefore (∃x)◻(Fx & E!x) and since we are in S5, ◊(∃x)◻(Fx & E!x).