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$$