Proving Math Logic: Solving the Existential Quantifier

[Dragonfall]

I need to prove the following:

$$\forall x\forall y[(fy=x)\rightarrow Qx]\vdash \exists xQx$$.

I can't do it.

 

[Dragonfall]

Is this even true? Seems a bit fishy.

 

[0rthodontist]

I take it f is a function. It shouldn't seem fishy--after all fy has to equal something (most logics contain the assumption that the universe contains at least one object), and whatever it equals must have property Q.

I am not familiar with the rules of your specific inference system. One plausible way, whether it's sufficiently formal for a logic derivation I do not know, is to instantiate the premise with y and fy, so you get
(fy = fy) -> Qfy
And maybe you have a premise that x = x for all x, so you could then derive Qfy
Then use existential generalization on fy (is this legal in your system?) to obtain
$$\exists$$x Qx