Metamath Proof Explorer

Theorem cardeqv

Description: All sets are well-orderable under choice. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion cardeqv 
|- dom card = _V

Proof

Step Hyp Ref Expression
1 axac3 
 |-  CHOICE
2 dfac10 
 |-  ( CHOICE <-> dom card = _V )
3 1 2 mpbi 
 |-  dom card = _V