Metamath Proof Explorer

Theorem acnum

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

Ref Expression
Assertion acnum 
|- ( CHOICE -> ( A e. V -> A e. dom card ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 dfac10 
 |-  ( CHOICE <-> dom card = _V )
3 2 biimpi 
 |-  ( CHOICE -> dom card = _V )
4 3 eleq2d 
 |-  ( CHOICE -> ( A e. dom card <-> A e. _V ) )
5 1 4 imbitrrid 
 |-  ( CHOICE -> ( A e. V -> A e. dom card ) )