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