I'm not sure what I'm missing here, but I have this lemma I am trying to prove, and it is giving me a lot of trouble. I'm technically working in ZF set theory, but this part doesn't need much more than basic predicate calculus (except for the defintion of a function). In symbols, I'd like to prove:
$$\forall x:P(x)\to Q(f(x))$$ $$\exists x:P(x)$$ $$\Rightarrow\exists y:Q(y)$$
In words, this says that if for every set $x$ that satisfies $P$ there is an associated set $y$ (which depends on $x$) which satisfies $Q$, and some set satisfies $P$, then some set also satisfies $Q$. This is intuitively obvious, as I can just find that $x$, so that the $f(x)$ associated to it satisfies $Q$, and so something satisfies $Q$. However, I'm having trouble getting from point A to point B using the axioms.
I'm working with Metamath, which has a fairly complete selection of axioms and theorems to work with, but it is still on a pretty basic level, so just make deductions you feel comfortable with, and I will tell you if I have difficulty with a hidden assumption being made.
Edit: An alternative formalization, which eliminates the function usage:
$$\forall a:P(a)\to Q$$ $$\exists x:P(x)$$ $$\Rightarrow Q$$
You are perhaps tripping over your own notation. The premiss you intend seems to be
$1.\quad\quad \forall x (P(x) \to Q(f(x))$
for some function $f$. You are also given
$2. \quad\quad \exists x P(x)$
So start a sub-proof by assuming
$3\quad\quad|\quad P(a)$
Then you can of course continue the proof
$4\quad\quad|\quad(P(a) \to Q(f(a))$
$5\quad\quad|\quad Q(f(a))$
But you have existential quantifier introduction in the form, if $\tau$ is a term, from $\varphi(\tau)$ you can infer $\exists \nu\varphi(\nu)$ for any [new] variable, so we have
$6\quad\quad|\quad \exists yQ(y)$
Given $\exists xP(x)$ and the subproof from (3) to (6) where the sub-proof's conclusion doesn't depend on $a$, the desired conclusion
$7\quad\quad \exists yQ(y)$
now follows by existential quantifier elimination. Job done!