Theorem acnum

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

	Ref	Expression
Assertion	acnum	⊢ ( CHOICE → ( 𝐴 ∈ 𝑉 → 𝐴 ∈ dom card ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		dfac10	⊢ ( CHOICE ↔ dom card = V )
3	2	biimpi	⊢ ( CHOICE → dom card = V )
4	3	eleq2d	⊢ ( CHOICE → ( 𝐴 ∈ dom card ↔ 𝐴 ∈ V ) )
5	1 4	imbitrrid	⊢ ( CHOICE → ( 𝐴 ∈ 𝑉 → 𝐴 ∈ dom card ) )