The proposition is:
If $f：X\rightarrow Y$is an onto, then $\exists X_1\subset X\ \text{s.t.}\ \text{card}(X_1)=\text{card}(Y)$ i.e. $\exists\ g: X_1\rightarrow Y$ is a bijection.
It could be proved with the Axiom of Choice as follows:
We define a relation on $X$: $x\sim y$ if $f(x) = f(y)$. It could be easily seen that "$\sim$" is an equivalence relation. With AC, we could “choose” one element from each equivalence class and define $X_1$ to be the set of the representatives we get. Then $f|_{X_1}: X_1\rightarrow Y$ is a bijection.
I wonder whether we could prove the proposition without the Axiom of Choice. We have proved that we could't disprove it under the ZF set theory. (If we could, since AC is a full condition of it, then we could disprove AC with the ZF axioms. Contradiction!)
Notice that in my description of the propsition $g$ may not be equal to $f|_{X_1}$, so the proposition is different from the similar one which is equivalent to AC.