>>104
>例えば、X✕Yの2つの要素について、
>同じxをもつものを同値とするなら
>各xについて、あるy0∈Yをとってきて
>(x,y0)を代表とすればいいだけ
>この場合は選択公理要らないですね

その例より下記だな?
下記”Polish space”=ポーランド空間
弥勒菩薩の住む世界だ

https://mathoverflow.net/questions/416407/unnecessary-uses-of-the-axiom-of-choice
Unnecessary uses of the axiom of choice Feb 17, 2022 Tom Leinster
What examples are there of habitual but unnecessary uses of the axiom of choice, in any area of mathematics except topology?

I'm interested in standard proofs that use the axiom of choice, but where choice can be eliminated via some judicious and maybe not quite obvious rephrasing. I'm less interested in proofs that were originally proved using choice and where it took some significant new idea to remove the dependence on choice.

I exclude topology because I already know lots of topological examples. For instance, Andrej Bauer's Five stages of accepting constructive mathematics gives choicey and choice-free proofs of a standard result (Theorem 1.4): every open cover of a compact metric space has a Lebesgue number. Todd Trimble told me about some other topological examples, e.g. a compact subspace of a Hausdorff space is closed, or the product of two compact spaces is compact. There are more besides.

To show what I'm looking for, here's an example taken from that paper of Andrej Bauer. It would qualify as an answer except that it comes from topology.
13
It is easy to prove the following in Z+CC (Zermelo plus countable choice):
Every uncountable closed set of reals is in bijection with the reals.
2 This is provable in Z,
even in second-order arithmetic. The principle ATR0 is equivalent to every uncountable closed set in a Polish space containing a perfect subset. –
Elliot Glazer Feb 18, 2022