Theorem acnum

Description: The Axiom of Choice implies that any set is numerable. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	acnum	$$⊢\mathrm{CHOICE}\to \left(A\in V\to A\in \mathrm{dom}\mathrm{card}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
3	2	biimpi	$$⊢\mathrm{CHOICE}\to \mathrm{dom}\mathrm{card}=\mathrm{V}$$
4	3	eleq2d	$$⊢\mathrm{CHOICE}\to \left(A\in \mathrm{dom}\mathrm{card}\leftrightarrow A\in \mathrm{V}\right)$$
5	1 4	imbitrrid	$$⊢\mathrm{CHOICE}\to \left(A\in V\to A\in \mathrm{dom}\mathrm{card}\right)$$