@SmootQ Hello Smoot. I was trying to work on this problem on my own and I think I managed to come up with something. I'd appreciate it if you can let me know if I managed to do this correctly. (Thanks in advance.)
So the problem was to go from ☐(x)(Fx ⊃ ☐(E!x & (E!x ⊃ Fx))) to ☐((∃x)Fx ⊃ ☐(∃x)Fx). The thought was to use a variable domain (free) quantified modal logic S5 system. Here's what I have tried doing:
We start with our premise ☐(x)(Fx ⊃ ☐(E!x & (E!x ⊃ Fx))). From this we can straightforwardly deduce that ☐((∃x)Fx ⊃ (∃x)☐(E!x & (E!x ⊃ Fx))). Call this N. I will come back to this later. Now we assume the consequent of this, i.e. (∃x)☐(E!x & (E!x ⊃ Fx)), for conditional proof.
Conditional proof: So we start with (∃x)☐(E!x & (E!x ⊃ Fx)). From this we can straightforwardly deduce that (∃x)☐(E!x & Fx). At this point using the free logic rule for existential generalization (since we have E!x) we can deduce that (∃x)☐(∃x)Fx. Since the first (∃x) now becomes redundant we can move to ☐(∃x)Fx. That completes our conditional proof. From (∃x)☐(E!x & (E!x ⊃ Fx)) we have deduced that ☐(∃x)Fx. Hence we conclude that (∃x)☐(E!x & (E!x ⊃ Fx)) ⊃ ☐(∃x)Fx.
Since we used nothing more than the rules of our logic to establish this conditional above then by necessitation rule we can move to ☐((∃x)☐(E!x & (E!x ⊃ Fx)) ⊃ ☐(∃x)Fx). Call this N'. Now from N (from above) and N' we can by transitivity of strict implication move to our conclusion ☐((∃x)Fx ⊃ ☐(∃x)Fx).
So, then, we have successfully deduced ☐((∃x)Fx ⊃ ☐(∃x)Fx) from our premise ☐(x)(Fx ⊃ ☐(E!x & (E!x ⊃ Fx))).